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

ex y being Element of E st y in rng R

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

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

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

then ex y being object st y in rng R by XBOOLE_0:def 1;

hence ex y being Element of E st y in rng R ; :: thesis: verum

ex y being Element of E st y in rng R

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

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

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

then ex y being object st y in rng R by XBOOLE_0:def 1;

hence ex y being Element of E st y in rng R ; :: thesis: verum