theorem :: MEASURE2:22

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 Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds
( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )