for r being Real
for seq being Real_Sequence holds
( ( for n being Nat holds seq . n <= r ) iff ( seq is V95() & upper_bound seq <= r ) )