:: deftheorem Def15 defines classical_octave MUSIC_S1:def 49 :
for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct holds
( MS is classical_octave iff for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Octave (MS,frequency) = 2 * fr ) );