for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~) .:^ (R .:^ X) & Y c= R .:^ ((R ~) .:^ Y) ) by Th60;