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