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

R is Relation of X,Y

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

assume ( dom R c= X & rng R c= Y ) ; :: thesis: R is Relation of X,Y

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

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

R is Relation of X,Y

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

assume ( dom R c= X & rng R c= Y ) ; :: thesis: R is Relation of X,Y

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

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