instance PiBase.instPrepathConnectedSpaceOfPresimplyConnectedSpace {X : Type u} [TopologicalSpace X] [h : PresimplyConnectedSpace X] : PrepathConnectedSpace X

Theorem T590: P200 (PreSimplyConnectedSpace) => P37 (PrePathConnectedSpace)

theorem PiBase.Formal.T590 : P200 ≤ P37