rng f = rng (Rev f) by Th8;
then rng (Rev f) c= D by RELAT_1:def 19;
hence Rev f is D -valued by RELAT_1:def 19; :: thesis: verum