theorem :: RELAT_1:118

for X being set
for R being Relation holds
( R .: X = {} iff dom R misses X )