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