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 set ; :: according to RELAT_1:def 3 :: thesis: for b being set st [x,b] in X | R holds
[x,b] in Y | R
let y be set ; :: 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 Def12;
hence ( [x,y] in X | R implies [x,y] in Y | R ) by A1, Def12; :: thesis: verum