Definition 1.1.3.  Let S be a set. We define:
S is empty  :⇔  S =   ⇔  S ⊆   ⇔  ∄ x ∈ S  ⇔  |S| = 0
S is nonempty  :⇔  S is not empty
Equivalence.
Remarks.

In HLM, multiple alternative definitions can be given for an operator or predicate, if they can be shown to be equal/equivalent. In proofs, the most convenient alternative can be selected at will, which reduces the number of necessary steps. Sometimes, it also makes sense to prove a property according to one alternative and then use it according to another.

References.