theorem :: MEASURE8:25

for X being set
for C being C_Measure of X
for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C