:: deftheorem Def12a defines satisfying_Nat MUSIC_S1:def 17 :
for S being MusicStruct holds
( S is satisfying_Nat iff NATPLUS c= the carrier of S );