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

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

now

assume A2: [x,y] in R ; :: thesis: [x,y] in Y1 | R
then y in Y by ZFMISC_1:106;
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 by RELAT_1:def 2; :: thesis: verum