theorem :: RELAT_1:105
for X, Y being set
for R being Relation holds (X \ Y) |` R = (X |` R) \ (Y |` R)