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