theorem :: RINFSUP1:23

for seq being Real_Sequence st seq is V55() & seq is V96() holds
seq is bounded ;