theorem Th73: :: RINFSUP1:73

for n being Nat
for seq being Real_Sequence st seq is V55() & seq is V96() holds
( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )