let X, X1, Y be set ; for R being Relation of X,Y holds R | X1 is Relation of X1,Y
let R be Relation of X,Y; R | X1 is Relation of X1,Y
now for x, y being object st [x,y] in R | X1 holds
[x,y] in [:X1,Y:]let x,
y be
object ;
( [x,y] in R | X1 implies [x,y] in [:X1,Y:] )assume
[x,y] in R | X1
;
[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;
verum end;
hence
R | X1 is Relation of X1,Y
by RELAT_1:def 3; verum