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