theorem Th23: :: RELSET_2:23

for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds
( (.: R) .: {_{X}_} = {} iff X = {} )