instance PiBase.instHasGδSingletonsOfGδSpaceOfT1Space {X : Type u} [TopologicalSpace X] [h : GδSpace X] [h' : T1Space X] : HasGδSingletons X

Theorem T502: P132 (GδSpace) + P2 (T1Space) => P191 (HasGδSingletons)

theorem PiBase.Formal.T502 : P132 ⊓ P2 ≤ P191