theorem PiBase.instDiscreteTopologyOfSubsingleton {X : Type u} [TopologicalSpace X] [Subsingleton X] : DiscreteTopology X

Theorem T248: ¬P125 (Nontrivial) => P52 (DiscreteTopology)

theorem PiBase.Formal.T248 : P125ᶜ ≤ P52