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