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

let x, y be set ; :: thesis: ( [x,y] in R | X1 implies [x,y] in [:X1,Y:] )
assume A2: [x,y] in R | X1 ; :: thesis: [x,y] in [:X1,Y:]
then A3: ( x in X1 & [x,y] in R ) by RELAT_1:def 11;
y in Y by A2, ZFMISC_1:106;
hence [x,y] in [:X1,Y:] by A3, ZFMISC_1:106; :: thesis: verum

end;

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