let x, y be object ; for R being Relation holds
( [x,y] in R iff y in Im (R,x) )
let R be Relation; ( [x,y] in R iff y in Im (R,x) )
thus
( [x,y] in R implies y in Im (R,x) )
( y in Im (R,x) implies [x,y] in R )
assume
y in Im (R,x)
; [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; verum