theorem PiBase.instT1SpaceOfT2Space {X : Type u} [TopologicalSpace X] [T2Space X] : T1Space X

Theorem T118: P3 (T2Space) => P2 (T1Space)

theorem PiBase.Formal.T118 : P3 ≤ P2