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