theorem Th67: :: RINFSUP1:67

for n being Nat
for seq being Real_Sequence st seq is non-decreasing & seq is bounded_above holds
( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )