instance PiBase.instWeaklyLocallySimplyConnectedSpaceOfLocallySimplyConnectedSpace {X : Type u_1} [TopologicalSpace X] [h : LocallySimplyConnectedSpace X] : WeaklyLocallySimplyConnectedSpace X

theorem PiBase.Formal.T853 : P230 ≤ P231