instance PiBase.instHasOpenConnectedComponentsOfHasOpenPathComponents {X : Type u} [TopologicalSpace X] [h : HasOpenPathComponents X] : HasOpenConnectedComponents X

Theorem T862: P233 (HasOpenPathComponents) => P234 (HasOpenConnectedComponents)

theorem PiBase.Formal.T862 : P233 ≤ P234