let X, Y be set ; :: thesis: for R being Relation holds (R " X) \ (R " Y) c= R " (X \ Y)
let R be Relation; :: thesis: (R " X) \ (R " Y) c= R " (X \ Y)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (R " X) \ (R " Y) or x in R " (X \ Y) )
assume A1: x in (R " X) \ (R " Y) ; :: thesis: x in R " (X \ Y)
then A2: ( x in R " X & not x in R " Y ) by XBOOLE_0:def 5;
consider y being set such that
A3: ( [x,y] in R & y in X ) by A1, Def14;
( not y in Y or not [x,y] in R ) by A2, Def14;
then ( y in X \ Y & [x,y] in R ) by A3, XBOOLE_0:def 5;
hence x in R " (X \ Y) by Def14; :: thesis: verum