for x, X being set holds
( x in the carrier of (EqRelLatt X) iff x is Equivalence_Relation of X )