theorem Th3: :: LIMFUNC1:3

for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing holds
for n being Nat holds 0 < seq . n