:: deftheorem Def17 defines Octave_descendent MUSIC_S1:def 51 :
for MS being satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct
for frequency, b₃ being Element of MS holds
( b₃ = Octave_descendent (MS,frequency) iff [b₃,frequency] in octave MS );