theorem PiBase.instInfiniteOfCountableInfinite {X : Type u} [CountablyInfinite X] : Infinite X

Theorem 455: a countable, infinite space is countably infinite

theorem PiBase.Formal.T455 : P181 ≤ P78ᶜ