theorem Th159: :: RELAT_1:169

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