theorem PiBase.instCardEqContinuumOfCardLeContinuumOfNotCardltContinuum {X : Type u} [h : CardLeContinuum X] (h' : ¬CardLtContinuum X) : CardEqContinuum X

Theorem 391: |X| ≤ 𝔠 and ¬ |X| < 𝔠 implies |X| = 𝔠

theorem PiBase.Formal.T391 : P163 ⊓ P58ᶜ ≤ P65