let A, x be set ; :: thesis: ( x in the carrier of (EqRelLATT A) iff x is Equivalence_Relation of A )

hereby :: thesis: ( x is Equivalence_Relation of A implies x in the carrier of (EqRelLATT A) )

assume x in the carrier of (EqRelLATT A) ; :: thesis: x is Equivalence_Relation of A
then reconsider e = x as Element of (LattPOSet (EqRelLatt A)) ;
% e = e ;
then A1: x in the carrier of (EqRelLatt A) ;
the carrier of (EqRelLatt A) = { r where r is Relation of A,A : r is Equivalence_Relation of A } by MSUALG_5:def 2;
then ex x9 being Relation of A,A st
( x9 = x & x9 is Equivalence_Relation of A ) by A1;
hence x is Equivalence_Relation of A ; :: thesis: verum

end;

A2: the carrier of (EqRelLatt A) = { r where r is Relation of A,A : r is Equivalence_Relation of A } by MSUALG_5:def 2;
assume x is Equivalence_Relation of A ; :: thesis: x in the carrier of (EqRelLATT A)
then x in the carrier of (EqRelLatt A) by A2;
then reconsider e = x as Element of (EqRelLatt A) ;
reconsider e = e as Element of (EqRelLATT A) ;
e in the carrier of (EqRelLATT A) ;
hence x in the carrier of (EqRelLATT A) ; :: thesis: verum