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 Def2;
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 ex x1 being Relation of X,X st
( x = x1 & x1 is Equivalence_Relation of X ) by A1;
hence x is Equivalence_Relation of X ; :: thesis: verum

end;

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