let X be set ; :: thesis: for P, R being Relation st P c= R holds
P | X c= R | X
let P, R be Relation; :: thesis: ( P c= R implies P | X c= R | X )
assume A1: P c= R ; :: thesis: P | X c= R | X
for x, y being set st [x,y] in P | X holds
[x,y] in R | X

proof

let x, y be set ; :: thesis: ( [x,y] in P | X implies [x,y] in R | X )
assume [x,y] in P | X ; :: thesis: [x,y] in R | X
then ( [x,y] in P & x in X ) by Def11;
hence [x,y] in R | X by A1, Def11; :: thesis: verum

end;

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