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