instance PiBase.instCardLeContinuumOfCardLePowerContinuum {X : Type u} [h : CardLeContinuum X] : CardLePowerContinuum X

Theorem 390: |X| ≤ 𝔠 implies |X| ≤ 2^𝔠

theorem PiBase.Formal.T390 : P163 ≤ P59