theorem :: RELAT_1:92

for Y being set
for R being Relation holds Y |` R = R * (id Y)