S variables_in t c= X by Th14;
then S variables_in t = X variables_in t by PBOOLE:23;
hence S variables_in t is ManySortedSubset of X ; :: thesis: verum