for seq being Real_Sequence holds
( seq is V96() iff rng seq is bounded_below )