theorem Th18: :: MEASURE2:18

for N being Function st ( for n being Nat holds N . n c= N . (n + 1) ) holds
for m, n being Nat st n <= m holds
N . n c= N . m