theorem Th34: :: RINFSUP1:34

for seq being Real_Sequence st seq is non-decreasing holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
lower_bound R = seq . n