instance PiBase.instLocallyConnectedSpaceOfPreirreducibleSpace {X : Type u} [TopologicalSpace X] [h : PreirreducibleSpace X] : LocallyConnectedSpace X

Theorem T51: P39 (PreirreducibleSpace) => P41 (LocallyConnectedSpace)

theorem PiBase.Formal.T51 : P39 ≤ P41