instance PiBase.instT1SpaceOfCountableSetsDiscrete {X : Type u} [TopologicalSpace X] [h : CountableSetsDiscrete X] : T1Space X

Theorem T221: P168 (CountableSetsDiscrete) => P2 (T1Space)

theorem PiBase.Formal.T221 : P168 ≤ P2