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 consider y being set such that
A2: [x,y] in P by Def4;
not x in dom R by A1, XBOOLE_0:def 5;
then not [x,y] in R by Def4;
then [x,y] in P \ R by A2, XBOOLE_0:def 5;
hence x in dom (P \ R) by Def4; :: thesis: verum