theorem Th12: :: SEQM_3:12

for seq being Real_Sequence st seq is non-increasing holds
for n being Nat holds seq . n <= seq . 0 by Th8;