theorem PiBase.instNotPreconnectedSpaceOfTotallyDisconnectedSpaceOfNontrivial {X : Type u} [TopologicalSpace X] [TotallyDisconnectedSpace X] [h : Nontrivial X] : ¬PreconnectedSpace X

Theorem T52: P47 (TotallyDisconnectedSpace) + P125 (Nontrivial) => ¬P36 (PreconnectedSpace)

theorem PiBase.Formal.T52 : P47 ⊓ P125 ≤ P36ᶜ