theorem Th13: :: MEASURE2:13

for N, F being Function st F . 0 = {} & ( for n being Nat holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds
for n being Nat holds F . n c= F . (n + 1)