for seq being Real_Sequence st seq is V95() & seq is nonnegative holds
upper_bound seq >= 0