instance PiBase.instCardLeContinuumOfCardEqAlephOne {X : Type u} [h : CardEqAlephOne X] : CardLeContinuum X

Theorem 190: ℵ₁ ≤ 𝔠

theorem PiBase.Formal.T190 : P114 ≤ P163