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