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