let D, E be non empty set ; :: thesis: 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 )
let R be Relation of D,E; :: thesis: for y being object holds
( y in rng R iff ex x being Element of D st [x,y] in R )
let y be object ; :: thesis: ( y in rng R iff ex x being Element of D st [x,y] in R )
thus ( y in rng R implies ex x being Element of D st [x,y] in R ) :: thesis: ( ex x being Element of D st [x,y] in R implies y in rng R )

proof

assume y in rng R ; :: thesis: ex x being Element of D st [x,y] in R
then consider x being object such that
A1: [x,y] in R by XTUPLE_0:def 13;
reconsider a = x as Element of D by A1, ZFMISC_1:87;
take a ; :: thesis: [a,y] in R
thus [a,y] in R by A1; :: thesis: verum

end;

thus ( ex x being Element of D st [x,y] in R implies y in rng R ) by XTUPLE_0:def 13; :: thesis: verum