for seq being Real_Sequence st seq is V55() & seq is V96() holds
lim seq = lower_bound seq