theorem Th15: :: RINFSUP1:15

for seq1, seq2 being Real_Sequence st seq1 is bounded_below & seq2 is bounded_below holds
lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2)