let P, R, Q be Relation; :: thesis: (P * R) \ (P * Q) c= P * (R \ Q)
let a be set ; :: according to RELAT_1:def 3 :: thesis: for b being set st [a,b] in (P * R) \ (P * Q) holds
[a,b] in P * (R \ Q)
let 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 consider y being set such that
A2: [a,y] in P and
A3: [y,b] in R by Def8;
not [a,b] in P * Q by A1, XBOOLE_0:def 5;
then ( not [a,y] in P or not [y,b] in Q ) by Def8;
then [y,b] in R \ Q by A2, A3, XBOOLE_0:def 5;
hence [a,b] in P * (R \ Q) by A2, Def8; :: thesis: verum