let x be object ; :: 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 object st [x,y] in R by XTUPLE_0:def 12;
hence Im (R,x) <> {} by Th159; :: thesis: verum

end;

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