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

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 )

hence
Y1 |` R = R
; :: thesis: verum( [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 )

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

hence
( [x,y] in Y1 |` R iff [x,y] in R )
by RELAT_1:def 12; :: thesis: verumassume 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;then y in Y by ZFMISC_1:87;

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