Description: Define the disjoint element relations class, i.e., the disjoint elements
class. The element of the disjoint elements class and the disjoint
elementhood predicate are the same, that is
( A e. ElDisjs <-> ElDisj A ) when A is a set, see
eleldisjseldisj . (Contributed by Peter Mazsa, 28-Nov-2022)