for seq being Real_Sequence holds
( ( seq is bounded & lim_sup seq = lim_inf seq ) iff seq is convergent )