:: deftheorem Def04 defines RAT_ratio MUSIC_S1:def 8 :
for x, y, b₃ being Element of RATPLUS holds
( b₃ = RAT_ratio (x,y) iff ex r, s being positive Rational st
( x = r & s = y & b₃ = s / r ) );