theorem Th11: :: TOPMETR3:11

for R being non empty Subset of REAL st R is bounded_above holds
ex s being Real_Sequence st
( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R )