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