theorem PiBase.instPseudocompactSpaceOfCountablyCompactSpace {X : Type u_1} [TopologicalSpace X] [hX : CountablyCompactSpace X] : PseudocompactSpace X

theorem PiBase.Formal.T4 : P19 ≤ P22