let P, R be Relation; :: thesis: dom (P /\ R) c= (dom P) /\ (dom R)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (P /\ R) or x in (dom P) /\ (dom R) )
assume x in dom (P /\ R) ; :: thesis: x in (dom P) /\ (dom R)
then consider y being set such that
A1: [x,y] in P /\ R by Def4;
( [x,y] in P & [x,y] in R ) by A1, XBOOLE_0:def 4;
then ( x in dom P & x in dom R ) by Def4;
hence x in (dom P) /\ (dom R) by XBOOLE_0:def 4; :: thesis: verum