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
for x, y being set st [x,y] in X | R holds
[x,y] in Y | R

proof

let x, 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

end;

hence X | R c= Y | R by Def3; :: thesis: verum