|Description: Define the empty set.
More precisely, we should write "empty class". It
will be posited in ax-nul 5027 that an empty set exists. Then, by
among classes (eq0 4157, as opposed to the weaker uniqueness among
nulmo 2761), it will follow that ∅ is indeed a set (0ex 5028).
case of Exercise 4.10(o) of [Mendelson]
p. 231. For a more traditional
definition, but requiring a dummy variable, see dfnul2 4143. (Contributed
by NM, 17-Jun-1993.) Clarify that at this point, it is not established
that it is a set. (Revised by BJ,