Definition 1.8.1.44.  Let M ⊆  such that M is finite and M is nonempty. For m ∈ M, we define:
max(M) = m  :⇔  ∀ n ∈ M : m ≥ n  ⇔  ∀ l ∈ M s.t. l ≥ m : l = m  ⇔  ∄ k ∈ M : k > m
Equivalence.  No proof.
Well-definedness.  No proof.
References.