:: deftheorem Def2 defines ascending REARRAN1:def 2 :
for IT being FinSequence holds
( IT is ascending iff for n being Nat st 1 <= n & n <= (len IT) - 1 holds
IT . n c= IT . (n + 1) );