theorem PiBase.instDowkerSpaceOfT4SpaceOfNotCountablyParacompactSpace {X : Type u} [TopologicalSpace X] [T4Space X] (h2 : ¬CountablyParacompactSpace X) : DowkerSpace X

Theorem T159: P7 (T4Space) + P32 (¬CountablyParacompactSpace) => P127 (DowkerSpace)

theorem PiBase.Formal.T159 : P7 ⊓ P32ᶜ ≤ P127