theorem Th16: :: RINFSUP1:16

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