theorem :: MEASURE2:17

for X being set
for S being SigmaField of X
for N, F being sequence of S st F . 0 = {} & ( for n being Nat holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds
rng F is non-decreasing N_Measure_fam of S