for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) )