theorem Th24: :: RINFSUP1:24

for seq being Real_Sequence st seq is V54() & seq is V95() holds
lim seq = upper_bound seq