let R1, R2 be Equivalence_Relation of (Frac S); ( ( for u, v being Element of Frac S holds
( [u,v] in R1 iff u,v Fr_Eq S ) ) & ( for u, v being Element of Frac S holds
( [u,v] in R2 iff u,v Fr_Eq S ) ) implies R1 = R2 )
assume that
A5:
for u, v being Element of Frac S holds
( [u,v] in R1 iff u,v Fr_Eq S )
and
A6:
for u, v being Element of Frac S holds
( [u,v] in R2 iff u,v Fr_Eq S )
; R1 = R2
for o, o1 being object holds
( [o,o1] in R1 iff [o,o1] in R2 )
proof
let o,
o1 be
object ;
( [o,o1] in R1 iff [o,o1] in R2 )
thus
(
[o,o1] in R1 implies
[o,o1] in R2 )
( [o,o1] in R2 implies [o,o1] in R1 )
assume A8:
[o,o1] in R2
;
[o,o1] in R1
then
(
o is
Element of
Frac S &
o1 is
Element of
Frac S )
by ZFMISC_1:87;
hence
[o,o1] in R1
by A5, A6, A8;
verum
end;
hence
R1 = R2
by RELAT_1:def 2; verum