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 frequency being Element of MS holds (@ ((spiral_of_fifths (MS,frequency,frequency)) . 4)) / (@ ((spiral_of_fifths (MS,frequency,frequency)) . 2)) = (3 * 3) / ((2 * 2) * 2)