:: deftheorem defines "increasing STIRL2_1:def 1 :
for n, k being Nat
for f being Function of (Segm n),(Segm k) holds
( f is "increasing iff ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( for l, m being Nat st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m}) ) ) );