:: deftheorem defines penta_3 MUSIC_S1:def 72 :
for MS being MusicSpace
for frequency being Element of MS holds penta_3 (MS,frequency) = (pentatonic_pythagorean_scale (MS,frequency)) . 4;