let x, y be object ; :: 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 Def11; :: thesis: verum

end;

assume y in Im (R,x) ; :: thesis: [x,y] in R
then ex z being object st
( [z,y] in R & z in {x} ) by Def11;
hence [x,y] in R by TARSKI:def 1; :: thesis: verum