let R be Relation; :: thesis: ( R is X -valued implies R is Y -valued )
assume R is X -valued ; :: thesis: R is Y -valued
then ( rng R c= X & X c= Y ) by RELAT_1:def 19;
then rng R c= Y by XBOOLE_1:1;
hence R is Y -valued by RELAT_1:def 19; :: thesis: verum