theorem PiBase.instT4SpaceOfDowkerSpace {X : Type u} [TopologicalSpace X] [DowkerSpace X] : T4Space X

Theorem T157: P127 (DowkerSpace) => P7 (T4Space)

theorem PiBase.Formal.T157 : P127 ≤ P7