theorem Th45: :: RINFSUP1:45

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