ex X being non empty set st the Instructions of S c= [:NAT,(NAT *),(X *):] by Def17;
then reconsider II = dom the Instructions of S as Relation ;
assume InsCodes S is empty ; :: thesis: contradiction
then II = {} ;
hence contradiction ; :: thesis: verum