theorem PiBase.instPreconnectedSpaceOfContinuumSpace {X : Type u} [TopologicalSpace X] [ContinuumSpace X] : PreconnectedSpace X

Theorem T483: P188 (ContinuumSpace) => P36 (PreconnectedSpace)

theorem PiBase.Formal.T483 : P188 ≤ P36