theorem Th21: :: MEASURE2:21

for X being set
for S being SigmaField of X
for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
F is Sep_Sequence of S