:: deftheorem defines ditonic MUSIC_S1:def 55 :
for MS being MusicSpace
for scale being Element of 3 -tuples_on the carrier of MS holds
( scale is ditonic iff ex frequency being Element of MS ex r1, r2, r3 being positive Real st
( scale . 1 = frequency & scale . 1 = r1 & scale . 2 = r2 & scale . 3 = r3 & r1 < r2 & r2 < r3 & scale . 3 = Octave (MS,frequency) ) );