instance PiBase.instHasGδSingletonsOfFirstCountableTopologyOfT1Space {X : Type u} [TopologicalSpace X] [FirstCountableTopology X] [T1Space X] : HasGδSingletons X

Theorem T501: P28 (FirstCountableTopology) + P2 (T1Space) => P191 (HasGδSingletons)

theorem PiBase.Formal.T501 : P28 ⊓ P2 ≤ P191