for seq being Real_Sequence st seq is convergent holds
( lim seq = lim_sup seq & lim seq = lim_inf seq )