for X, Y being set
for R being Relation holds (R |_2 X) |_2 Y = R |_2 (X /\ Y)