theorem PiBase.instT2SpaceOfT25Space {X : Type u} [TopologicalSpace X] [T25Space X] : T2Space X

Theorem T32: P4 (T25Space) => P3 (T2Space)

theorem PiBase.Formal.T32 : P4 ≤ P3