let Y be set ; for E1, E2 being Equivalence_Relation of Y st Class E1 = Class E2 holds
E1 = E2
let E1, E2 be Equivalence_Relation of Y; ( Class E1 = Class E2 implies E1 = E2 )
assume A1:
Class E1 = Class E2
; E1 = E2
now for x being object holds
( ( x in E1 implies x in E2 ) & ( x in E2 implies x in E1 ) )let x be
object ;
( ( x in E1 implies x in E2 ) & ( x in E2 implies x in E1 ) )hereby ( x in E2 implies x in E1 )
assume A2:
x in E1
;
x in E2then 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;
verum
end; assume A8:
x in E2
;
x in E1then 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;
verum end;
hence
E1 = E2
; verum