theorem PiBase.instPreconnectedSpaceOfHasACutPoint {X : Type u} [TopologicalSpace X] [HasACutPoint X] : PreconnectedSpace X

Theorem T452: P204 (HasACutPoint) => P36 (PreconnectedSpace)

theorem PiBase.Formal.T452 : P204 ≤ P36