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 A2: [x,y] in Y1 | R ; :: thesis: [x,y] in [:X,Y1:]
then A3: ( y in Y1 & [x,y] in R ) by RELAT_1:def 12;
x in X by A2, ZFMISC_1:106;
hence [x,y] in [:X,Y1:] by A3, ZFMISC_1:106; :: thesis: verum

end;

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