theorem Th9: :: RELSET_2:9

for x, y being object
for R being Relation holds
( y in Im (R,x) iff [x,y] in R )