theorem :: RINFSUP1:76

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V96() & seq2 is V96() holds
(inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)