theorem PiBase.instNotCountablyParacompactSpaceOfDowkerSpace {X : Type u} [TopologicalSpace X] [DowkerSpace X] : ¬CountablyParacompactSpace X

Theorem T158: P127 (DowkerSpace) => P32 (¬CountablyParacompactSpace)

theorem PiBase.Formal.T158 : P127 ≤ P32ᶜ