let X, Y be set ; :: thesis: for R being Relation st X c= Y holds
R | X c= R | Y
let R be Relation; :: thesis: ( X c= Y implies R | X c= R | Y )
assume A1: X c= Y ; :: thesis: R | X c= R | Y
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b being set st [x,b] in R | X holds
[x,b] in R | Y
let y be set ; :: thesis: ( [x,y] in R | X implies [x,y] in R | Y )
assume [x,y] in R | X ; :: thesis: [x,y] in R | Y
then ( x in X & [x,y] in R ) by Def11;
hence [x,y] in R | Y by A1, Def11; :: thesis: verum