A1: rng q c= D by RELAT_1:def 19;
( rng (p ^ q) = (rng p) \/ (rng q) & rng p c= D ) by Th24, RELAT_1:def 19;
hence p ^ q is D -valued by A1, XBOOLE_1:8; :: thesis: verum