theorem PiBase.le_one_iff_subsingleton {α : Type u} : Cardinal.mk α ≤ 1 ↔ Subsingleton α

theorem PiBase.one_lt_iff_nontrivial {α : Type u} : 1 < Cardinal.mk α ↔ Nontrivial α

instance PiBase.instNontrivialOfCardGeThree {X : Type u} [h : CardGeThree X] : Nontrivial X

Theorem 428: |X| ≥ 3 implies X has multiple points

theorem PiBase.Formal.T428 : P175 ≤ P125