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

now :: thesis: for x, y being object st [x,y] in R | X1 holds
[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;

hence R | X1 is Relation of X1,Y by RELAT_1:def 3; :: thesis: verum