for Y being set
for R being Relation holds Y |` R c= R by Def10;