theorem PiBase.instCountableOfCountablyInfiniteOfCountablyInfinite {X : Type u} [CountablyInfinite X] : Countable X

Theorem 454: Countably infinite implies countable

theorem PiBase.Formal.T454 : P181 ≤ P57