for seq being Real_Sequence st seq is V96() holds
(inferior_realsequence seq) . 0 = lower_bound seq