for Y being set
for P, R being Relation holds (Y |` R) * P c= R * P by Th24, Th80;