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