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

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

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

end;

A2: the carrier of (EqRelLatt A) = { r where r is Relation of , : r is Equivalence_Relation of } by MSUALG_5:def 2;
assume x is Equivalence_Relation of ; :: 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 ;
reconsider e = e as Element of ;
e in the carrier of (EqRelLATT A) ;
hence x in the carrier of (EqRelLATT A) ; :: thesis: verum