theorem Th123: :: RELAT_1:131

for Y being set
for x being object
for R being Relation holds
( x in R " Y iff ex y being object st
( y in rng R & [x,y] in R & y in Y ) )