theorem :: RELSET_1:25

for D, E being non empty set
for R being Relation of D,E
for y being object holds
( y in rng R iff ex x being Element of D st [x,y] in R )