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