instance PiBase.instCardGeFourOfNotFinite {X : Type u} [h : Infinite X] : CardGeFour X

Theorem 431: X infinite implies 4 ≤ |X|

theorem PiBase.Formal.T431 : P78ᶜ ≤ P176