instance PiBase.instSeqCompactSpaceCountablyCompactSpace {X : Type u_1} [TopologicalSpace X] [SeqCompactSpace X] : CountablyCompactSpace X

Theorem T3: P20 (Sequentially compact) => P19 (Countably compact) --This is in mathlib (but not in stable version).

theorem PiBase.Formal.T3 : P20 ≤ P19