for MS1, MS2 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 frequency1 being Element of MS1
for frequency2 being Element of MS2 st frequency1 = frequency2 holds
Octave_descendent (MS1,frequency1) = Octave_descendent (MS2,frequency2)