theorem PiBase.instT5SpaceOfT1SpaceOfCompletelyNormalSpace {X : Type u} [TopologicalSpace X] [T1Space X] [CompletelyNormalSpace X] : T5Space X

Theorem T101: P2 (T1Space) + P14 (CompletelyNormalSpace) => P8 (T5Space)

theorem PiBase.Formal.T101 : P2 ⊓ P14 ≤ P8