instance PiBase.instCardLeContinuumOfCardEqContinuum {X : Type u} [h : CardEqContinuum X] : CardLeContinuum X

Theorem 139: |X| = 𝔠 implies |X| ≤ 𝔠

theorem PiBase.Formal.T139 : P65 ≤ P163