for r being Real
for seq being Real_Sequence st seq is V95() holds
( r = upper_bound seq iff ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) ) )