theorem Th44: :: RINFSUP1:44

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