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