theorem :: MEASURE9:39

for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for F being disjoint_valued FinSequence of S
for R being non empty preBoolean Subset-Family of X st S c= R & Union F in R holds
for i being Nat holds Union (F | i) in R