:: deftheorem defines increasing EUCLID_7:def 1 :
for h being real-valued FinSequence holds
( h is increasing iff for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1) );