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

proof

assume A2: [x,y] in EqR ; :: thesis: Class EqR,x = Class EqR,y

now

let z be set ; :: thesis: ( z in Class EqR,y implies z in Class EqR,x )
assume z in Class EqR,y ; :: thesis: z in Class EqR,x
then A3: [z,y] in EqR by Th27;
[y,x] in EqR by A2, Th12;
then [z,x] in EqR by A3, Th13;
hence z in Class EqR,x by Th27; :: thesis: verum

end;

then A4: Class EqR,y c= Class EqR,x by TARSKI:def 3;

now

let z be set ; :: thesis: ( z in Class EqR,x implies z in Class EqR,y )
assume z in Class EqR,x ; :: thesis: z in Class EqR,y
then [z,x] in EqR by Th27;
then [z,y] in EqR by A2, Th13;
hence z in Class EqR,y by Th27; :: thesis: verum

end;

then Class EqR,x c= Class EqR,y by TARSKI:def 3;
hence Class EqR,x = Class EqR,y by A4, XBOOLE_0:def 10; :: thesis: verum

end;

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