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