for MS being MusicSpace
for f1, f2 being Element of MS ex r1, r2 being Element of REALPLUS st intrval (f1,f2) = REAL_ratio (r1,r2)