for N being Nat
for seq being Real_Sequence of N st seq is convergent holds
seq is bounded