let P, R, Q be Relation; :: thesis: (P * R) \ (P * Q) c= P * (R \ Q)

now

let a, b be set ; :: thesis: ( [a,b] in (P * R) \ (P * Q) implies [a,b] in P * (R \ Q) )
assume A1: [a,b] in (P * R) \ (P * Q) ; :: thesis: [a,b] in P * (R \ Q)
then A2: ( [a,b] in P * R & not [a,b] in P * Q ) by XBOOLE_0:def 5;
consider y being set such that
A3: ( [a,y] in P & [y,b] in R ) by A1, Def8;
( not [a,y] in P or not [y,b] in Q ) by A2, Def8;
then [y,b] in R \ Q by A3, XBOOLE_0:def 5;
hence [a,b] in P * (R \ Q) by A3, Def8; :: thesis: verum

end;

hence (P * R) \ (P * Q) c= P * (R \ Q) by Def3; :: thesis: verum