let X, Y, Y1 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 )

A1: dom R c= X by RELAT_1:def 18;

assume rng R c= Y1 ; :: thesis: R is Relation of X,Y1

then ( R c= [:(dom R),(rng R):] & [:(dom R),(rng R):] c= [:X,Y1:] ) by A1, RELAT_1:7, ZFMISC_1:96;

hence R is Relation of X,Y1 by XBOOLE_1:1; :: thesis: verum

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 )

A1: dom R c= X by RELAT_1:def 18;

assume rng R c= Y1 ; :: thesis: R is Relation of X,Y1

then ( R c= [:(dom R),(rng R):] & [:(dom R),(rng R):] c= [:X,Y1:] ) by A1, RELAT_1:7, ZFMISC_1:96;

hence R is Relation of X,Y1 by XBOOLE_1:1; :: thesis: verum