theorem Th5: :: MEASURE2:5

for X being set
for S being non empty Subset-Family 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)) \/ (F . n) ) holds
for r being set
for n being Nat holds
( r in F . n iff ex k being Nat st
( k <= n & r in N . k ) )