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