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

let R be Relation of X,Y; :: thesis: R | X1 is Relation of X1,Y

let R be Relation of X,Y; :: thesis: R | X1 is Relation of X1,Y

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

[x,y] in [:X1,Y:]

hence
R | X1 is Relation of X1,Y
by RELAT_1:def 3; :: thesis: verum[x,y] in [:X1,Y:]

let x, y be object ; :: thesis: ( [x,y] in R | X1 implies [x,y] in [:X1,Y:] )

assume [x,y] in R | X1 ; :: thesis: [x,y] in [:X1,Y:]

then ( x in X1 & y in Y ) by RELAT_1:def 11, ZFMISC_1:87;

hence [x,y] in [:X1,Y:] by ZFMISC_1:87; :: thesis: verum

end;assume [x,y] in R | X1 ; :: thesis: [x,y] in [:X1,Y:]

then ( x in X1 & y in Y ) by RELAT_1:def 11, ZFMISC_1:87;

hence [x,y] in [:X1,Y:] by ZFMISC_1:87; :: thesis: verum