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

let x be set ; :: 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 set such that
A3: ( x = [a,b] & a in Y & b in Y ) by RELSET_1:6;
reconsider a = a, b = b as Element of Y by A3;
A4: b in Class E1,b by A3, EQREL_1:28;
A5: a in Class E1,b by A2, A3, EQREL_1:27;
Class E1,b in Class E2 by A1, A3, EQREL_1:def 5;
then consider c being set such that
A6: ( c in Y & Class E1,b = Class E2,c ) by EQREL_1:def 5;
( [a,c] in E2 & [b,c] in E2 ) by A4, A5, A6, EQREL_1:27;
then ( [a,c] in E2 & [c,b] in E2 ) by EQREL_1:12;
hence x in E2 by A3, EQREL_1:13; :: thesis: verum

end;

assume A7: x in E2 ; :: thesis: x in E1
then consider a, b being set such that
A8: ( x = [a,b] & a in Y & b in Y ) by RELSET_1:6;
reconsider a = a, b = b as Element of Y by A8;
A9: b in Class E2,b by A8, EQREL_1:28;
A10: a in Class E2,b by A7, A8, EQREL_1:27;
Class E2,b in Class E1 by A1, A8, EQREL_1:def 5;
then consider c being set such that
A11: ( c in Y & Class E2,b = Class E1,c ) by EQREL_1:def 5;
( [a,c] in E1 & [b,c] in E1 ) by A9, A10, A11, EQREL_1:27;
then ( [a,c] in E1 & [c,b] in E1 ) by EQREL_1:12;
hence x in E1 by A8, EQREL_1:13; :: thesis: verum

end;

hence E1 = E2 by TARSKI:2; :: thesis: verum