let R1, R2 be Equivalence_Relation of (Frac S); :: thesis: ( ( 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 ) ; :: thesis: R1 = R2
for o, o1 being object holds
( [o,o1] in R1 iff [o,o1] in R2 )

proof

let o, o1 be object ; :: thesis: ( [o,o1] in R1 iff [o,o1] in R2 )
thus ( [o,o1] in R1 implies [o,o1] in R2 ) :: thesis: ( [o,o1] in R2 implies [o,o1] in R1 )

proof

assume A7: [o,o1] in R1 ; :: thesis: [o,o1] in R2
then ( o is Element of Frac S & o1 is Element of Frac S ) by ZFMISC_1:87;
hence [o,o1] in R2 by A5, A6, A7; :: thesis: verum

end;

assume A8: [o,o1] in R2 ; :: thesis: [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; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum