Description: This (useless) theorem, which was proved without the Axiom of Infinity,
demonstrates an artifact of our definition of binary relation, which is
meaningful only when its arguments exist. In particular, the antecedent
cannot be satisfied unless _om exists. (Contributed by NM, 13-Nov-2003)