let X, Y be set ; :: thesis: for R being Relation holds R | (X \ Y) = (R | X) \ (R | Y)
let R be Relation; :: thesis: R | (X \ Y) = (R | X) \ (R | Y)
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in R | (X \ Y) iff [x,b] in (R | X) \ (R | Y) )
let y be set ; :: thesis: ( [x,y] in R | (X \ Y) iff [x,y] in (R | X) \ (R | Y) )

hereby :: thesis: ( [x,y] in (R | X) \ (R | Y) implies [x,y] in R | (X \ Y) )

assume A2: [x,y] in R | (X \ Y) ; :: thesis: [x,y] in (R | X) \ (R | Y)
then A3: x in X \ Y by Def11;
then not x in Y by XBOOLE_0:def 5;
then A4: not [x,y] in R | Y by Def11;
[x,y] in R by A2, Def11;
then [x,y] in R | X by A3, Def11;
hence [x,y] in (R | X) \ (R | Y) by A4, XBOOLE_0:def 5; :: thesis: verum

end;

assume A5: [x,y] in (R | X) \ (R | Y) ; :: thesis: [x,y] in R | (X \ Y)
then A6: [x,y] in R by Def11;
not [x,y] in R | Y by A5, XBOOLE_0:def 5;
then A7: ( not x in Y or not [x,y] in R ) by Def11;
x in X by A5, Def11;
then x in X \ Y by A5, A7, Def11, XBOOLE_0:def 5;
hence [x,y] in R | (X \ Y) by A6, Def11; :: thesis: verum