theorem PiBase.instPreconnectedSpaceOfSigmaConnectedSpace {X : Type u} [TopologicalSpace X] [SigmaConnectedSpace X] : PreconnectedSpace X

Theorem T484: P189 (SigmaConnectedSpace) => P36 (PreconnectedSpace)

theorem PiBase.Formal.T484 : P189 ≤ P36