for seq being Real_Sequence st seq is V95() holds
(superior_realsequence seq) . 0 = upper_bound seq