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 )
assume A1: dom R c= X1 ; :: thesis: R is Relation of X1,Y
A2: R c= [:(dom R),(rng R):] by RELAT_1:21;
rng R c= Y by RELAT_1:def 19;
then [:(dom R),(rng R):] c= [:X1,Y:] by A1, ZFMISC_1:119;
hence R is Relation of X1,Y by A2, XBOOLE_1:1; :: thesis: verum