instance PiBase.instHasOpenConnectedComponentsOfPreconnectedSpace {X : Type u} [TopologicalSpace X] [h : PreconnectedSpace X] : HasOpenConnectedComponents X

Theorem T864: P36 (PreconnectedSpace) => P234 (HasOpenConnectedComponents)

theorem PiBase.Formal.T864 : P36 ≤ P234