theorem PiBase.instT1SpaceOfDiscreteTopology {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : T1Space X

Theorem T42: P52 (DiscreteTopology) => P2 (T1Space)

theorem PiBase.Formal.T42 : P52 ≤ P2