theorem :: MEASUR10:24

for X being set
for S being non empty cap-closed semi-diff-closed Subset-Family of X
for E1, E2 being Element of S ex F1, F2, F3 being disjoint_valued FinSequence of S st
( union (rng F1) = E1 \ E2 & union (rng F2) = E2 \ E1 & union (rng F3) = E1 /\ E2 & (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S )