theorem :: MEASURE2:9

for X being set
for S being SigmaField of X
for N being sequence of S ex F being sequence of S st
( F . 0 = {} & ( for n being Nat holds F . (n + 1) = (N . 0) \ (N . n) ) )