instance PiBase.instCountablyInfiniteOfCountableOfInfinite {X : Type u} [Countable X] [Infinite X] : CountablyInfinite X

Theorem 456: a countably infinite space is infinite

theorem PiBase.Formal.T456 : P57 ⊓ P78ᶜ ≤ P181