theorem :: ORDERS_1:83

for R being Relation
for X being set holds (R |_2 X) ~ = (R ~) |_2 X by Lm16;