take f = the empty one-to-one Function; :: thesis: ( f is empty & f is X -defined & f is Y -valued & f is one-to-one )
( dom f = {} & rng f = {} ) ;
hence ( f is empty & f is X -defined & f is Y -valued & f is one-to-one ) by RELAT_1:def 18, RELAT_1:def 19, XBOOLE_1:2; :: thesis: verum