theorem :: RELAT_1:138

for Y being set
for R being Relation holds
( R " Y = {} iff rng R misses Y )