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