let y be set ; :: thesis: for R being Relation holds
( y in rng R iff R " {y} <> {} )
let R be Relation; :: thesis: ( y in rng R iff R " {y} <> {} )
thus ( y in rng R implies R " {y} <> {} ) :: thesis: ( R " {y} <> {} implies y in rng R )

proof

assume y in rng R ; :: thesis: R " {y} <> {}
then consider x being set such that
A1: [x,y] in R by RELAT_1:def 5;
y in {y} by TARSKI:def 1;
hence R " {y} <> {} by A1, RELAT_1:def 14; :: thesis: verum

end;

assume R " {y} <> {} ; :: thesis: y in rng R
then consider x being set such that
A2: x in R " {y} by XBOOLE_0:def 1;
consider z being set such that
A3: [x,z] in R and
A4: z in {y} by A2, RELAT_1:def 14;
z = y by A4, TARSKI:def 1;
hence y in rng R by A3, RELAT_1:def 5; :: thesis: verum