:: deftheorem Def21 defines intrval MUSIC_S1:def 63 :
for MS being MusicSpace
for f1, f2 being Element of MS
for b₄ being positive Real holds
( b₄ = intrval (f1,f2) iff ex r1, r2 being positive Real st
( r1 = f1 & r2 = f2 & b₄ = r2 / r1 ) );