theorem Th83: :: MUSIC_S1:102

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds (spiral_of_fifths (HPS,frequency,(Fourth (HPS,frequency)))) . 2 = (3 / 2) * (@ frequency)