let R1, R2 be Relation of [:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:]; :: thesis: ( ( for x, y being Element of [:REALPLUS,REALPLUS:] holds
( [x,y] in R1 iff ex a, b, c, d being Element of REALPLUS st
( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) ) ) & ( for x, y being Element of [:REALPLUS,REALPLUS:] holds
( [x,y] in R2 iff ex a, b, c, d being Element of REALPLUS st
( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) ) ) implies R1 = R2 )
assume that
A2: for x, y being Element of [:REALPLUS,REALPLUS:] holds
( [x,y] in R1 iff ex a, b, c, d being Element of REALPLUS st
( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) ) and
A3: for x, y being Element of [:REALPLUS,REALPLUS:] holds
( [x,y] in R2 iff ex a, b, c, d being Element of REALPLUS st
( x = [a,b] & y = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) ) ; :: thesis: R1 = R2
for x, y being object holds
( [x,y] in R1 iff [x,y] in R2 )

proof

let x, y be object ; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )

hereby :: thesis: ( [x,y] in R2 implies [x,y] in R1 )

assume A4: [x,y] in R1 ; :: thesis: [x,y] in R2
then reconsider x9 = x, y9 = y as Element of [:REALPLUS,REALPLUS:] by ZFMISC_1:87;
ex a, b, c, d being Element of REALPLUS st
( x9 = [a,b] & y9 = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) by A4, A2;
hence [x,y] in R2 by A3; :: thesis: verum

end;

assume A5: [x,y] in R2 ; :: thesis: [x,y] in R1
then reconsider x9 = x, y9 = y as Element of [:REALPLUS,REALPLUS:] by ZFMISC_1:87;
ex a, b, c, d being Element of REALPLUS st
( x9 = [a,b] & y9 = [c,d] & REAL_ratio (a,b) = REAL_ratio (c,d) ) by A3, A5;
hence [x,y] in R1 by A2; :: thesis: verum

end;

hence R1 = R2 ; :: thesis: verum