Definition 1.8.1.42.  Let M ⊆  such that M is nonempty. For m ∈ M, we define:
min(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.