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

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