instance PiBase.instPrepathconnectedSpaceOfPreconnectedSpaceOfHasOpenPathComponents {X : Type u} [TopologicalSpace X] [h : PreconnectedSpace X] [h' : HasOpenPathComponents X] : PrepathConnectedSpace X

Theorem T95: P36 (PreconnectedSpace) + P233 (HasOpenPathComponents) => P37 (PrepathConnectedSpace)

theorem PiBase.Formal.T95 : P36 ⊓ P233 ≤ P37