:: deftheorem Def01 defines REAL_ratio MUSIC_S1:def 4 :
for x, y, b₃ being Element of REALPLUS holds
( b₃ = REAL_ratio (x,y) iff ex r, s being positive Real st
( x = r & s = y & b₃ = s / r ) );