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