instance PiBase.instWeaklyCountablyCompactOfCountablyCompactSpace {X : Type u_1} [TopologicalSpace X] [hX : CountablyCompactSpace X] : WeaklyCountablyCompact X

Theorem T2: P19 (Countably compact) => P21 (Weakly countably compact)

theorem PiBase.Formal.T2 : P19 ≤ P21