instance PiBase.instPreconnectedSpaceOfPrepathConnectedSpace {X : Type u} [TopologicalSpace X] [PrepathConnectedSpace X] : PreconnectedSpace X

Theorem T40: P37 (PrepathConnectedSpace) => P36 (PreconnectedSpace)

theorem PiBase.Formal.T40 : P37 ≤ P36