theorem Th16: :: MEASUR11:22

for X, Y being non empty set
for A being Subset of X
for B being Subset of Y
for p being set holds
( ( p in A implies X-section ([:A,B:],p) = B ) & ( not p in A implies X-section ([:A,B:],p) = {} ) & ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )