let R1, R2 be Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:]; :: thesis: ( ( 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) ) ) ; :: 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 [: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; :: thesis: verum
end;
assume A5: [x,y] in R2 ; :: thesis: [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; :: thesis: verum
end;
hence R1 = R2 ; :: thesis: verum