:: deftheorem defines penta_octave MUSIC_S1:def 74 :
for MS being MusicSpace
for frequency being Element of MS holds penta_octave (MS,frequency) = Octave (MS,frequency);