set S = Trivial-AMI N;
A1: the carrier of (Trivial-AMI N) = succ NAT by Def2;
thus not the carrier of (Trivial-AMI N) is empty by Def2; :: according to STRUCT_0:def 1 :: thesis: Trivial-AMI N is stored-program
thus NAT c= the carrier of (Trivial-AMI N) by A1, XBOOLE_1:7; :: according to AMI_1:def 3 :: thesis: verum