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