theorem Th19: :: MEASUR11:25

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