let Y, Y1, X 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

let x, y be set ; :: 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