theorem PiBase.instT1SpaceOfT4Space {X : Type u} [TopologicalSpace X] [T4Space X] : T1Space X

Theorem T98: P7 (T4Space) => P2 (T1Space)

theorem PiBase.Formal.T98 : P7 ≤ P2