let X, Y be set ; :: thesis: for R being Relation holds (X \ Y) |` R = (X |` R) \ (Y |` R)
let R be Relation; :: thesis: (X \ Y) |` R = (X |` R) \ (Y |` R)
let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in (X \ Y) |` R iff [x,b] in (X |` R) \ (Y |` R) )
let y be object ; :: thesis: ( [x,y] in (X \ Y) |` R iff [x,y] in (X |` R) \ (Y |` R) )
A1: ( y in X \ Y iff ( y in X & not y in Y ) ) by XBOOLE_0:def 5;
A2: ( [x,y] in (X |` R) \ (Y |` R) iff ( [x,y] in X |` R & not [x,y] in Y |` R ) ) by XBOOLE_0:def 5;
( [x,y] in X |` R iff ( y in X & [x,y] in R ) ) by Def10;
hence ( [x,y] in (X \ Y) |` R iff [x,y] in (X |` R) \ (Y |` R) ) by A1, A2, Def10; :: thesis: verum