theorem :: MUSIC_S1:112

for HPS being satisfying_euclidean Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds heptatonic_pythagorean_scale (HPS,frequency) is perfect_fifth