let R1, R2 be Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:]; ( ( for x, y being Element of [:RATPLUS,RATPLUS:] holds
( [x,y] in R1 iff ex a, b, c, d being Element of RATPLUS st
( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) ) ) & ( for x, y being Element of [:RATPLUS,RATPLUS:] holds
( [x,y] in R2 iff ex a, b, c, d being Element of RATPLUS st
( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) ) ) implies R1 = R2 )
assume that
A2:
for x, y being Element of [:RATPLUS,RATPLUS:] holds
( [x,y] in R1 iff ex a, b, c, d being Element of RATPLUS st
( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) )
and
A3:
for x, y being Element of [:RATPLUS,RATPLUS:] holds
( [x,y] in R2 iff ex a, b, c, d being Element of RATPLUS st
( x = [a,b] & y = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) ) )
; R1 = R2
for x, y being object holds
( [x,y] in R1 iff [x,y] in R2 )
proof
let x,
y be
object ;
( [x,y] in R1 iff [x,y] in R2 )
hereby ( [x,y] in R2 implies [x,y] in R1 )
assume A4:
[x,y] in R1
;
[x,y] in R2then reconsider x9 =
x,
y9 =
y as
Element of
[:RATPLUS,RATPLUS:] by ZFMISC_1:87;
ex
a,
b,
c,
d being
Element of
RATPLUS st
(
x9 = [a,b] &
y9 = [c,d] &
RAT_ratio (
a,
b)
= RAT_ratio (
c,
d) )
by A4, A2;
hence
[x,y] in R2
by A3;
verum
end;
assume A5:
[x,y] in R2
;
[x,y] in R1
then reconsider x9 =
x,
y9 =
y as
Element of
[:RATPLUS,RATPLUS:] by ZFMISC_1:87;
ex
a,
b,
c,
d being
Element of
RATPLUS st
(
x9 = [a,b] &
y9 = [c,d] &
RAT_ratio (
a,
b)
= RAT_ratio (
c,
d) )
by A3, A5;
hence
[x,y] in R1
by A2;
verum
end;
hence
R1 = R2
; verum