:: deftheorem Def07a defines satisfying_Real MUSIC_S1:def 12 :
for S being MusicStruct holds
( S is satisfying_Real iff the carrier of S c= REALPLUS );