theorem Th50: :: RINFSUP1:50
for seq being Real_Sequence st seq is V96() holds
inferior_realsequence seq is V54() by Th48;