theorem Th45: :: RELSET_2:45

for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )