:: deftheorem defines increasing VALUED_1:def 13 :
for X being non empty ext-real-membered set
for s being sequence of X holds
( s is increasing iff for n being Nat holds s . n < s . (n + 1) );