instance PiBase.instHasGδSingletonsOfLocallyCountableSpaceOfT1Space {X : Type u} [TopologicalSpace X] [h : LocallyCountableSpace X] [h' : T1Space X] : HasGδSingletons X

Theorem T790: P93 (LocallyCountableSpace) + P2 (T1Space) => P191 (HasGδSingletons)

theorem PiBase.Formal.T790 : P93 ⊓ P2 ≤ P191