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 R by A1, XBOOLE_0:def 4;
then A2: x in dom R by Def4;
[x,y] in P by A1, XBOOLE_0:def 4;
then x in dom P by Def4;
hence x in (dom P) /\ (dom R) by A2, XBOOLE_0:def 4; :: thesis: verum