for X, Y, Y1 being set
for R being Relation of X,Y holds Y1 |` R is Relation of X,Y1