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

now

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

now

assume A2: [x,y] in R ; :: thesis: [x,y] in R | X1
then x in X by ZFMISC_1:106;
hence [x,y] in R | X1 by A1, A2, RELAT_1:def 11; :: thesis: verum

end;

hence ( [x,y] in R | X1 iff [x,y] in R ) by RELAT_1:def 11; :: thesis: verum

end;

hence R | X1 = R by RELAT_1:def 2; :: thesis: verum