theorem PiBase.instNotHasAnIsolatedPointOfIndiscreteTopologyOfNontrivial {X : Type u} [TopologicalSpace X] [h : IndiscreteTopology X] [h' : Nontrivial X] : ¬HasAnIsolatedPoint X

Theorem T208: P129 (IndiscreteTopology) + P125 (Nontrivial) => P139 (¬HasAnIsolatedPoint)

theorem PiBase.Formal.T208 : P129 ⊓ P125 ≤ P139ᶜ