defpred S₁[ object , object ] means ex a, b, c, d being Element of RATPLUS st
( $1 = [a,b] & $2 = [c,d] & RAT_ratio (a,b) = RAT_ratio (c,d) );
consider R being Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] such that
A1: for x, y being object holds
( [x,y] in R iff ( x in [:RATPLUS,RATPLUS:] & y in [:RATPLUS,RATPLUS:] & S₁[x,y] ) ) from RELSET_1:sch 1();
for x, y being Element of [:RATPLUS,RATPLUS:] holds
( [x,y] in R 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) ) ) by A1;
hence ex b₁ being Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] st
for x, y being Element of [:RATPLUS,RATPLUS:] holds
( [x,y] in b₁ 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: verum