for seq being Real_Sequence st seq is bounded holds
( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) )