theorem PiBase.instNotCountableOfCardEqAlephOne {X : Type u} [h : CardEqAlephOne X] : ¬Countable X

Theorem 191: ℵ₁ is uncountable

theorem PiBase.Formal.T191 : P114 ≤ P57ᶜ