theorem Th53: :: RELAT_1:59

for X being set
for R being Relation holds R | X c= R by Def9;