theorem Th20: :: MUSIC_S1:24

for S being satisfying_Nat MusicStruct
for n being non zero Nat holds n is Element of S