let Y be set ; :: thesis: for E1, E2 being Equivalence_Relation of Y st Class E1 = Class E2 holds
E1 = E2
let E1, E2 be Equivalence_Relation of Y; :: thesis: ( Class E1 = Class E2 implies E1 = E2 )
assume A1: Class E1 = Class E2 ; :: thesis: E1 = E2

now :: thesis: for x being object holds
( ( x in E1 implies x in E2 ) & ( x in E2 implies x in E1 ) )

let x be object ; :: thesis: ( ( x in E1 implies x in E2 ) & ( x in E2 implies x in E1 ) )

hereby :: thesis: ( x in E2 implies x in E1 )

assume A2: x in E1 ; :: thesis: x in E2
then consider a, b being object such that
A3: x = [a,b] and
A4: a in Y and
A5: b in Y by RELSET_1:2;
reconsider a = a, b = b as Element of Y by A4, A5;
Class (E1,b) in Class E2 by A1, A4, EQREL_1:def 3;
then consider c being object such that
c in Y and
A6: Class (E1,b) = Class (E2,c) by EQREL_1:def 3;
b in Class (E1,b) by A4, EQREL_1:20;
then [b,c] in E2 by A6, EQREL_1:19;
then A7: [c,b] in E2 by EQREL_1:6;
a in Class (E1,b) by A2, A3, EQREL_1:19;
then [a,c] in E2 by A6, EQREL_1:19;
hence x in E2 by A3, A7, EQREL_1:7; :: thesis: verum

end;

assume A8: x in E2 ; :: thesis: x in E1
then consider a, b being object such that
A9: x = [a,b] and
A10: a in Y and
A11: b in Y by RELSET_1:2;
reconsider a = a, b = b as Element of Y by A10, A11;
Class (E2,b) in Class E1 by A1, A10, EQREL_1:def 3;
then consider c being object such that
c in Y and
A12: Class (E2,b) = Class (E1,c) by EQREL_1:def 3;
b in Class (E2,b) by A10, EQREL_1:20;
then [b,c] in E1 by A12, EQREL_1:19;
then A13: [c,b] in E1 by EQREL_1:6;
a in Class (E2,b) by A8, A9, EQREL_1:19;
then [a,c] in E1 by A12, EQREL_1:19;
hence x in E1 by A9, A13, EQREL_1:7; :: thesis: verum

end;

hence E1 = E2 ; :: thesis: verum