let X be set ; :: thesis: for R being Relation holds R | X c= R
let R be Relation; :: thesis: R | X c= R
for x, y being set st [x,y] in R | X holds
[x,y] in R by Def11;
hence R | X c= R by Def3; :: thesis: verum