for A, B being set
for R being Subset of [:A,B:]
for Y being set holds (R ~) .: Y = (R ~) .: (Y /\ (proj2 R))