let Y, Y1, X be set ; :: thesis: for R being Relation of X,Y st rng R c= Y1 holds
R is Relation of X,Y1
let R be Relation of X,Y; :: thesis: ( rng R c= Y1 implies R is Relation of X,Y1 )
assume A1: rng R c= Y1 ; :: thesis: R is Relation of X,Y1
A2: R c= [:(dom R),(rng R):] by RELAT_1:21;
dom R c= X by RELAT_1:def 18;
then [:(dom R),(rng R):] c= [:X,Y1:] by A1, ZFMISC_1:119;
hence R is Relation of X,Y1 by A2, XBOOLE_1:1; :: thesis: verum