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

proof

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

end;

assume A1: [x,y] in R ; :: thesis: y in Im (R,x)
x in {x} by TARSKI:def 1;
hence y in Im (R,x) by A1, RELAT_1:def 13; :: thesis: verum