instance PiBase.instCardLtContinuumOfCountable {X : Type u} [h : Countable X] : CardLtContinuum X

Theorem 67: Countable implies |X| < 𝔠

theorem PiBase.Formal.T67 : P57 ≤ P58