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