theorem :: RELSET_1:32

for A, X, Y being set
for P being Relation of X,Y st A misses X holds
P | A = {}