theorem :: MUSIC_S1:100

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS
for n being Nat holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . n is_Between frequency, Octave (HPS,frequency) by Th57, Th81;