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

Theorem T253: P125 (Nontrivial) + P1 (T0Space) => ¬P129 (IndiscreteTopology)

theorem PiBase.Formal.T253 : P125 ⊓ P1 ≤ P129ᶜ