let E, D be non empty set ; :: thesis: for R being Relation of D,E
for y being set 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 set holds
( y in rng R iff ex x being Element of D st [x,y] in R )
let y be set ; :: 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 set such that
A1: [x,y] in R by RELAT_1:def 5;
reconsider a = x as Element of D by A1, ZFMISC_1:106;
take a ; :: thesis: [a,y] in R
thus [a,y] in R by A1; :: thesis: verum

end;

given x being Element of D such that A2: [x,y] in R ; :: thesis: y in rng R
thus y in rng R by A2, RELAT_1:20; :: thesis: verum