theorem Th4: :: SEQM_3:4

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