let X, Y, Y1 be set ; :: thesis: for R being Relation of X,Y st Y c= Y1 holds
Y1 |` R = R
let R be Relation of X,Y; :: thesis: ( Y c= Y1 implies Y1 |` R = R )
assume A1: Y c= Y1 ; :: thesis: Y1 |` R = R

now :: thesis: for x, y being object holds
( [x,y] in Y1 |` R iff [x,y] in R )

let x, y be object ; :: thesis: ( [x,y] in Y1 |` R iff [x,y] in R )

now :: thesis: ( [x,y] in R implies [x,y] in Y1 |` R )

assume A2: [x,y] in R ; :: thesis: [x,y] in Y1 |` R
then y in Y by ZFMISC_1:87;
hence [x,y] in Y1 |` R by A1, A2, RELAT_1:def 12; :: thesis: verum

end;

hence ( [x,y] in Y1 |` R iff [x,y] in R ) by RELAT_1:def 12; :: thesis: verum

end;

hence Y1 |` R = R ; :: thesis: verum