:: deftheorem defines 'increasing STIRL2_1:def 3 :
for Ne, Ke being Subset of NAT
for f being Function of Ne,Ke holds
( f is 'increasing iff for l, m being Nat st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m}) );