Proposition 1.8.1.24.  Let M ⊆ . Then the following are equivalent:
  1. M is finite
  2. M is empty or ∃ m ∈ M : m is a ≤-greatest element of M
  3. M is empty or ∃! m ∈ M : m is a ≤-greatest element of M
  4. ∃ a ∈  : M ⊆ a
  5. ∃ b ∈  : M ⊆ <b
Proof.