theorem Th80: :: RELAT_1:86

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