theorem :: SEQM_3:9

for seq being Real_Sequence st seq is increasing holds
for n being Nat st 0 < n holds
seq . 0 < seq . n by Th1;