:: deftheorem Def16 defines satisfying_octave_descendent_constructible MUSIC_S1:def 50 :
for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct holds
( MS is satisfying_octave_descendent_constructible iff for frequency being Element of MS ex o being Element of MS st [o,frequency] in octave MS );