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 consider y being set such that
W: [x,y] in R by Def4;
y in Im R,x by W, Th204;
hence Im R,x <> {} ; :: thesis: verum

end;

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