theorem :: RINFSUP1:70

for seq being Real_Sequence st seq is V55() holds
superior_realsequence seq = seq