let x, y be set ; :: thesis: for R being Relation holds
( [x,y] in R iff y in Im R,x )
let R be Relation; :: thesis: ( [x,y] in R iff y in Im R,x )
thus ( [x,y] in R implies y in Im R,x ) :: thesis: ( y in Im R,x implies [x,y] in R )

proof

x in {x} by TARSKI:def 1;
hence ( [x,y] in R implies y in Im R,x ) by Def13; :: thesis: verum

end;

assume y in Im R,x ; :: thesis: [x,y] in R
then consider z being set such that
W1: [z,y] in R and
W2: z in {x} by Def13;
z = x by W2, TARSKI:def 1;
hence [x,y] in R by W1; :: thesis: verum