let X, Y be set ; for R being Relation st X c= Y holds
X |` R c= Y |` R
let R be Relation; ( X c= Y implies X |` R c= Y |` R )
assume A1:
X c= Y
; X |` R c= Y |` R
let x be object ; RELAT_1:def 3 for b being object st [x,b] in X |` R holds
[x,b] in Y |` R
let y be object ; ( [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; verum