ex X being non empty set st the Instructions of S c= [:NAT,(NAT *),(X *):] by Def17;
hence the Instructions of S is Relation-like ; :: thesis: verum