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