theorem PiBase.instNotPreconnectedOfR0SpaceOfHasAnIsolatedPointOfNontrivial {X : Type u} [TopologicalSpace X] [R0Space X] [HasAnIsolatedPoint X] [h : Nontrivial X] : ¬PreconnectedSpace X

Theorem T308: R₀ (P135) + Has an isolated point (P139) + Nontivial (P125) => Not Connected (P26)

theorem PiBase.Formal.T308 : P135 ⊓ P139 ⊓ P125 ≤ P36ᶜ