let X, X1, Y, Y1 be set ; :: thesis: for R being Relation of X,Y st X c= X1 & Y c= Y1 holds
R is Relation of X1,Y1
let R be Relation of X,Y; :: thesis: ( X c= X1 & Y c= Y1 implies R is Relation of X1,Y1 )
assume ( X c= X1 & Y c= Y1 ) ; :: thesis: R is Relation of X1,Y1
then [:X,Y:] c= [:X1,Y1:] by ZFMISC_1:96;
hence R is Relation of X1,Y1 by XBOOLE_1:1; :: thesis: verum