theorem Th16: :: RINFSUP1:16

for seq1, seq2 being Real_Sequence st seq1 is bounded_above & seq2 is bounded_above holds
upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2)