theorem :: RELAT_1:187
for X, Y being set
for P, R being Relation st X misses Y holds
P | X misses R | Y