:: deftheorem Def03 defines EQUIV_REAL_ratio MUSIC_S1:def 6 :
for b₁ being Relation of [:REALPLUS,REALPLUS:],[:REALPLUS,REALPLUS:] holds
( b₁ = EQUIV_REAL_ratio iff for x, y being Element of [:REALPLUS,REALPLUS:] holds
( [x,y] in b₁ 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) ) ) );