:: deftheorem defines penta_1 MUSIC_S1:def 70 :
for MS being MusicSpace
for frequency being Element of MS holds penta_1 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 2;