theorem Th19: :: STIRL2_1:19

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
min* (f " {m}) <= (n - k) + m