let P, R be Relation; :: thesis: ( dom P misses dom R implies P misses R )
assume A1: dom P misses dom R ; :: thesis: P misses R

now

given x being set such that A2: x in dom (P /\ R) ; :: thesis: contradiction
dom (P /\ R) c= (dom P) /\ (dom R) by RELAT_1:14;
hence contradiction by A1, A2, XBOOLE_0:def 7; :: thesis: verum

end;

hence P /\ R = {} by XBOOLE_0:def 1; :: according to XBOOLE_0:def 7 :: thesis: verum