theorem :: RELAT_1:13

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