theorem Th41: :: RINFSUP1:41

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