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