theorem :: RELAT_1:14

for P, R being Relation holds (rng P) \ (rng R) c= rng (P \ R) by XTUPLE_0:29;