theorem Th17: :: SEQ_2:17

for seq being Real_Sequence st seq is convergent & ( for n being Nat holds 0 <= seq . n ) holds
0 <= lim seq