theorem PiBase.instIndiscreteTopologyOfSubsingleton {X : Type u} [TopologicalSpace X] [Subsingleton X] : IndiscreteTopology X

Theorem T249: ¬P125 (Nontrivial) => P129 (IndiscreteTopology)

theorem PiBase.Formal.T249 : P125ᶜ ≤ P129