let X, Y, Y1 be set ; :: thesis: for R being Relation of X,Y holds Y1 |` R is Relation of X,Y1
let R be Relation of X,Y; :: thesis: Y1 |` R is Relation of X,Y1

now :: thesis: for x, y being object st [x,y] in Y1 |` R holds
[x,y] in [:X,Y1:]

let x, y be object ; :: thesis: ( [x,y] in Y1 |` R implies [x,y] in [:X,Y1:] )
assume [x,y] in Y1 |` R ; :: thesis: [x,y] in [:X,Y1:]
then ( y in Y1 & x in X ) by RELAT_1:def 12, ZFMISC_1:87;
hence [x,y] in [:X,Y1:] by ZFMISC_1:87; :: thesis: verum

end;

hence Y1 |` R is Relation of X,Y1 by RELAT_1:def 3; :: thesis: verum