set p2 = rng P;
set q2 = rng Q;
set R = P * Q;
set r2 = rng (P * Q);
( rng (P * Q) c= rng Q & rng Q is trivial ) by RELAT_1:26, Def37;
hence P * Q is constanT ; :: thesis: verum