theorem Th7: :: MEASURE2:7

for X being set
for S being non empty Subset-Family of X
for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds
for n, m being Nat st n <= m holds
F . n c= G . m