theorem Th51: :: RINFSUP1:51

for seq being Real_Sequence st seq is V95() holds
superior_realsequence seq is V55() by Th49;