let X, X1, Y be set ; :: thesis: for R being Relation of X,Y st dom R c= X1 holds

R is Relation of X1,Y

let R be Relation of X,Y; :: thesis: ( dom R c= X1 implies R is Relation of X1,Y )

A1: rng R c= Y by RELAT_1:def 19;

assume dom R c= X1 ; :: thesis: R is Relation of X1,Y

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

hence R is Relation of X1,Y by XBOOLE_1:1; :: thesis: verum

R is Relation of X1,Y

let R be Relation of X,Y; :: thesis: ( dom R c= X1 implies R is Relation of X1,Y )

A1: rng R c= Y by RELAT_1:def 19;

assume dom R c= X1 ; :: thesis: R is Relation of X1,Y

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

hence R is Relation of X1,Y by XBOOLE_1:1; :: thesis: verum