theorem Th17: :: MEASUR11:23

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