theorem :: RELAT_1:170

for x being object
for R being Relation holds
( x in dom R iff Im (R,x) <> {} )