let x, X be set ; :: thesis: ( x in the carrier of (EqRelLatt X) iff x is Equivalence_Relation of X )
A1: the carrier of (EqRelLatt X) = { x1 where x1 is Relation of X,X : x1 is Equivalence_Relation of X } by MSUALG_5:def 2;
thus ( x in the carrier of (EqRelLatt X) implies x is Equivalence_Relation of X ) :: thesis: ( x is Equivalence_Relation of X implies x in the carrier of (EqRelLatt X) )

proof

assume x in the carrier of (EqRelLatt X) ; :: thesis: x is Equivalence_Relation of X
then consider x1 being Relation of X,X such that
A2: ( x = x1 & x1 is Equivalence_Relation of X ) by A1;
thus x is Equivalence_Relation of X by A2; :: thesis: verum

end;

thus ( x is Equivalence_Relation of X implies x in the carrier of (EqRelLatt X) ) by A1; :: thesis: verum