theorem PiBase.instT0SpaceOfT1Space {X : Type u} [TopologicalSpace X] [T1Space X] : T0Space X

Theorem T119: P2 (T1Space) => P1 (T0Space)

theorem PiBase.Formal.T119 : P2 ≤ P1