theorem :: RELAT_1:152

for f being Relation
for X being set st X misses dom f holds
f | X = {}