dom T = [#] V by Th7;
hence T " X is Subset of by RELAT_1:167; :: thesis: verum