let X, X1, Y 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 :: thesis: for x, y being object holds
( [x,y] in R | X1 iff [x,y] in R )
let x, y be object ; :: thesis: ( [x,y] in R | X1 iff [x,y] in R )
now :: thesis: ( [x,y] in R implies [x,y] in R | X1 )
assume A2: [x,y] in R ; :: thesis: [x,y] in R | X1
then x in X by ZFMISC_1:87;
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 ; :: thesis: verum