for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for frequency being Element of MS ex r being positive Real st
( frequency = r & Octave_descendent (MS,frequency) = r / 2 )