set dp = dom P;
set dq = dom Q;
set rp = rng P;
set rq = rng Q;
set R = P \/ Q;
reconsider p = P \ [:(dom Q),(rng P):] as Subset of P ;
( p c= P & P null Q c= P \/ Q ) ;
then reconsider p = p as Subset of (P \/ Q) by XBOOLE_1:1;
reconsider QQ = Q null P as Subset of (P \/ Q) ;
(p \/ QQ) \ (P \/ Q) = {} ;
hence P +*1 Q is Subset of (P \/ Q) ; :: thesis: verum