theorem PiBase.instT4SpaceOfT5Space {X : Type u} [TopologicalSpace X] [T5Space X] : T4Space X

Theorem T112: P8 (T5Space) => P7 (T4Space)

theorem PiBase.Formal.T112 : P8 ≤ P7