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 object ; :: 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 consider y being object such that
A2: [x,y] in R and
A3: y in X by Def12;
not x in R " Y by A1, XBOOLE_0:def 5;
then ( not y in Y or not [x,y] in R ) by Def12;
then y in X \ Y by A2, A3, XBOOLE_0:def 5;
hence x in R " (X \ Y) by A2, Def12; :: thesis: verum