instance PiBase.instSubsingletonOfDiscreteTopologyOfIndiscreteTopology {X : Type u} [TopologicalSpace X] [DiscreteTopology X] [h : IndiscreteTopology X] : Subsingleton X

Theorem T247: P52 (DiscreteTopology) + P129 (IndiscreteTopology) => ¬P125 (Nontrivial)

theorem PiBase.Formal.T247 : P52 ⊓ P129 ≤ P125ᶜ