Description: The following series of theorems are centered around the empty domain,
where no set exists. As a consequence, a set variable like x has no
instance to assign to. An expression like x = y is not really
meaningful then. What does it evaluate to, true or false? In fact, the
grammar extension weq requires us to formally assign a boolean value
to an equation, say always false, unless you want to give up on
exmid , for example. Whatever it is, we start out with the
contraposition of ax-6 , that guarantees the existence of at least one
set. Our hypothesis here expresses tentatively it might not hold. We
can simplify the antecedent then, to the point where we do not need
equation any more. This suggests what a decent characterization of the
empty domain of discourse could be. (Contributed by Wolf Lammen, 12-Mar-2023)