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

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:]

hence
Y1 |` R is Relation of X,Y1
by RELAT_1:def 3; :: thesis: verum[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;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