theorem :: RELAT_1:11

for P, R being Relation st P c= R holds
( dom P c= dom R & rng P c= rng R ) by XTUPLE_0:8, XTUPLE_0:9;