theorem Th22: :: WELLORD1:22

for Y, Z being set
for R being Relation st Z c= Y holds
(R |_2 Y) |_2 Z = R |_2 Z