let X, y be set ; :: thesis: for EqR being Equivalence_Relation of X
for x being set st x in X holds
( y in Class EqR,x iff Class EqR,x = Class EqR,y )
let EqR be Equivalence_Relation of X; :: thesis: for x being set st x in X holds
( y in Class EqR,x iff Class EqR,x = Class EqR,y )
let x be set ; :: thesis: ( x in X implies ( y in Class EqR,x iff Class EqR,x = Class EqR,y ) )
assume A1: x in X ; :: thesis: ( y in Class EqR,x iff Class EqR,x = Class EqR,y )
thus ( y in Class EqR,x implies Class EqR,x = Class EqR,y ) :: thesis: ( Class EqR,x = Class EqR,y implies y in Class EqR,x )

proof

assume y in Class EqR,x ; :: thesis: Class EqR,x = Class EqR,y
then [y,x] in EqR by Th27;
then [x,y] in EqR by Th12;
hence Class EqR,x = Class EqR,y by A1, Lm2; :: thesis: verum

end;

assume Class EqR,x = Class EqR,y ; :: thesis: y in Class EqR,x
then [x,y] in EqR by A1, Lm2;
then [y,x] in EqR by Th12;
hence y in Class EqR,x by Th27; :: thesis: verum