let x be set ; :: thesis: for R being Relation holds
( x in dom R iff Im (R,x) <> {} )
let R be Relation; :: thesis: ( x in dom R iff Im (R,x) <> {} )
thus ( x in dom R implies Im (R,x) <> {} ) :: thesis: ( Im (R,x) <> {} implies x in dom R )

proof

assume x in dom R ; :: thesis: Im (R,x) <> {}
then ex y being set st [x,y] in R by Def4;
hence Im (R,x) <> {} by Th204; :: thesis: verum

end;

assume Im (R,x) <> {} ; :: thesis: x in dom R
then consider y being set such that
A1: y in Im (R,x) by XBOOLE_0:def 1;
[x,y] in R by A1, Th204;
hence x in dom R by Def4; :: thesis: verum