Description: Define the coelement equivalence relation predicate. (Read: the coelement
equivalence relation on A .) Alternate definition is dfcoeleqvrel .
For sets, being an element of the class of coelement equivalence relations
is equivalent to satisfying the coelement equivalence relation predicate,
see elcoeleqvrelsrel . (Contributed by Peter Mazsa, 11-Dec-2021)