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

Theorem T99: P2 (T1Space) + P13 (NormalSpace) => P7 (T4Space)

theorem PiBase.Formal.T99 : P2 ⊓ P13 ≤ P7