let D, E be non empty set ; :: thesis: for R being Relation of D,E st rng R <> {} holds

ex x being Element of D st x in dom R

let R be Relation of D,E; :: thesis: ( rng R <> {} implies ex x being Element of D st x in dom R )

assume rng R <> {} ; :: thesis: ex x being Element of D st x in dom R

then dom R <> {} by RELAT_1:42;

then ex x being object st x in dom R by XBOOLE_0:def 1;

hence ex x being Element of D st x in dom R ; :: thesis: verum

ex x being Element of D st x in dom R

let R be Relation of D,E; :: thesis: ( rng R <> {} implies ex x being Element of D st x in dom R )

assume rng R <> {} ; :: thesis: ex x being Element of D st x in dom R

then dom R <> {} by RELAT_1:42;

then ex x being object st x in dom R by XBOOLE_0:def 1;

hence ex x being Element of D st x in dom R ; :: thesis: verum