let X, Y be set ; for R being Relation holds (X \ Y) |` R = (X |` R) \ (Y |` R)
let R be Relation; (X \ Y) |` R = (X |` R) \ (Y |` R)
let x be object ; RELAT_1:def 2 for b being object holds
( [x,b] in (X \ Y) |` R iff [x,b] in (X |` R) \ (Y |` R) )
let y be object ; ( [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; verum