theorem :: RINFSUP1:22

for seq being Real_Sequence st seq is V54() & seq is V95() holds
seq is bounded ;