theorem Th1: :: SEQM_3:1

for seq being Real_Sequence holds
( seq is increasing iff for n, m being Nat st n < m holds
seq . n < seq . m )