( rng <%d1%> = {d1} & {d1} c= D ) by Th36, ZFMISC_1:37;
hence <%d1%> is D -valued by RELAT_1:def 19; :: thesis: verum