for X, Y being set
for R being Relation st Y c= X holds
Y |` (X |` R) = Y |` R