Definition 1.8.2.17.  Let κ be a cardinal number. We define:
κ is finite  :⇔  κ ∈   ⇔  ∃ x ∈  : κ = x  ⇔  ∃ y ∈  : κ ≤ y  ⇔  ∃ z ∈  : κ < z
κ is infinite  :⇔  κ is not finite
Equivalence.  No proof.