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
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )