instance PiBase.instHasOpenPathComponentsOfLocallyPathConnectedSpace {X : Type u} [TopologicalSpace X] [h : LocallyPathConnectedSpace X] : HasOpenPathComponents X

Theorem T861: P42 (LocallyPathConnectedSpace) => P233 (HasOpenPathComponents)

theorem PiBase.Formal.T861 : P42 ≤ P233