:: deftheorem Def06 defines EQUIV_RAT_ratio MUSIC_S1:def 10 :
for b₁ being Relation of [:RATPLUS,RATPLUS:],[:RATPLUS,RATPLUS:] holds
( b₁ = EQUIV_RAT_ratio iff 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) ) ) );