theorem :: RELAT_1:122
for X, Y being set
for R being Relation holds (R .: X) \ (R .: Y) c= R .: (X \ Y)