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

then S variables_in t = X variables_in t by PBOOLE:23;

hence S variables_in t is ManySortedSubset of X ; :: thesis: verum