instance PiBase.instHasOpenConnectedComponentsOfLocallyConnectedSpace {X : Type u} [TopologicalSpace X] [h : LocallyConnectedSpace X] : HasOpenConnectedComponents X

Theorem T863: P41 (LocallyConnectedSpace) => P234 (HasOpenConnectedComponents)

theorem PiBase.Formal.T863 : P41 ≤ P234