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 y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (R .: X) \ (R .: Y) or y in R .: (X \ Y) )
assume A1: y in (R .: X) \ (R .: Y) ; :: thesis: y in R .: (X \ Y)
then A2: ( y in R .: X & not y in R .: Y ) by XBOOLE_0:def 5;
consider x being set such that
A3: ( [x,y] in R & x in X ) by A1, Def13;
( not x in Y or not [x,y] in R ) by A2, Def13;
then ( x in X \ Y & [x,y] in R ) by A3, XBOOLE_0:def 5;
hence y in R .: (X \ Y) by Def13; :: thesis: verum