instance PiBase.instDiscreteTopologyOfPSpaceOfHasGδSingletons {X : Type u} [TopologicalSpace X] [h : PSpace X] [h' : HasGδSingletons X] : DiscreteTopology X

Theorem T510: P147 (P space) + P191 (Has points Gδ) => P52 (Discrete)

theorem PiBase.Formal.T510 : P147 ⊓ P191 ≤ P52