:: deftheorem defines hepta_4 MUSIC_S1:def 85 :
for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds hepta_4 (HPS,frequency) = (heptatonic_pythagorean_scale (HPS,frequency)) . 5;