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