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