theorem Th18: :: STIRL2_1:18

for k, n being Nat
for f being Function of (Segm n),(Segm k) st f is onto & f is "increasing holds
for m being Nat st m < k holds
m <= min* (f " {m})