theorem Th7: :: RINFSUP1:7

for r being Real
for seq being Real_Sequence st seq is bounded_above 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 ) ) )