thus the Instructions of SCM c= [:NAT ,(((union {INT }) \/ the carrier of SCM ) * ):] ; :: according to AMI_1:def 32 :: thesis: ( not SCM is empty & SCM is stored-program )
thus ( not SCM is empty & SCM is stored-program ) by AMI_1:def 3, STRUCT_0:def 1; :: thesis: verum