:: deftheorem defines heptatonic_pythagorean_scale_ascending MUSIC_S1:def 90 :
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds heptatonic_pythagorean_scale_ascending (HPS,frequency) = heptatonic_pythagorean_scale (HPS,(Octave (HPS,frequency)));