instance PiBase.instT1SpaceOfHasGδSingletons {X : Type u} [TopologicalSpace X] [h : HasGδSingletons X] : T1Space X

Theorem T500: P191 (HasGδSingletons) => P2 (T1Space)

theorem PiBase.Formal.T500 : P191 ≤ P2