instance PiBase.instWeaklyLocallySimplyConnectedSpaceOfSimplyConnectedSpace {X : Type u_1} [TopologicalSpace X] [h : PresimplyConnectedSpace X] : WeaklyLocallySimplyConnectedSpace X

theorem PiBase.Formal.T858 : P200 ≤ P231