for MS being non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible classical_fifth satisfying_octave_constructible classical_octave satisfying_octave_descendent_constructible MusicStruct
for fondamentale, frequency being Element of MS st frequency is_Between fondamentale, Octave (MS,fondamentale) holds
for n being Nat holds (spiral_of_fifths (MS,fondamentale,frequency)) . n is_Between fondamentale, Octave (MS,fondamentale)