for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is non-decreasing holds
seq + seq1 is bounded_below