theorem Th40: :: RINFSUP1:40

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