theorem :: MEASUR11:24

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