for seq being Real_Sequence holds
( seq is V95() iff rng seq is bounded_above )