theorem :: WELLORD1:21

for Y being set
for R being Relation holds (R |_2 Y) |_2 Y = R |_2 Y