theorem Th19: :: WELLORD1:19

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