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