for seq being Real_Sequence st seq is V96() & seq is nonnegative holds
lower_bound seq >= 0 by Th10;