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