:: deftheorem Def14 defines Octave MUSIC_S1:def 47 :
for MS being satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_octave_constructible MusicStruct
for frequency, b₃ being Element of MS holds
( b₃ = Octave (MS,frequency) iff [frequency,b₃] in octave MS );