:: deftheorem defines @ MUSIC_S1:def 48 :
for MS being non empty satisfying_Real MusicStruct
for r being Element of MS holds @ r = r;