let R be Relation; :: thesis: for Y being set st rng R c= Y holds
R " Y = dom R
let Y be set ; :: thesis: ( rng R c= Y implies R " Y = dom R )
assume rng R c= Y ; :: thesis: R " Y = dom R
then (rng R) /\ Y = rng R by XBOOLE_1:28;
hence R " Y = R " (rng R) by RELAT_1:133
.= dom R by RELAT_1:134 ;
:: thesis: verum