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)

now

let x, y be set ; :: thesis: ( [x,y] in R | (X \ Y) iff [x,y] in (R | X) \ (R | Y) )

A1: now

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

end;

now

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

end;

hence ( [x,y] in R | (X \ Y) iff [x,y] in (R | X) \ (R | Y) ) by A1; :: thesis: verum

end;

hence R | (X \ Y) = (R | X) \ (R | Y) by Def2; :: thesis: verum