let S be satisfying_Nat MusicStruct ; :: thesis: for n being non zero Nat holds n is Element of S
let n be non zero Nat; :: thesis: n is Element of S
A1: NATPLUS c= the carrier of S by Def12a;
n in NATPLUS by NAT_LAT:def 6;
hence n is Element of S by A1; :: thesis: verum