instance PiBase.instCardLeContinuumOfCardLtContinuum {X : Type u} [h : CardLtContinuum X] : CardLeContinuum X

Theorem 68: < 𝔠 implies ≤ 𝔠

theorem PiBase.Formal.T68 : P58 ≤ P163