instance PiBase.instCompactSpaceOfCountablyCompactSpace {X : Type u_1} [TopologicalSpace X] [h : CompactSpace X] : CountablyCompactSpace X

theorem PiBase.Formal.T1 : P16 ≤ P19