:: deftheorem defines is_Between MUSIC_S1:def 45 :
for MS being MusicStruct
for a, b, c being Element of MS holds
( b is_Between a,c iff ex r1, r2, r3 being positive Real st
( a = r1 & b = r2 & c = r3 & r1 <= r2 & r2 < r3 ) );