for R being non empty Subset of REAL st R is bounded_below holds
ex s being Real_Sequence st
( s is non-increasing & s is convergent & rng s c= R & lim s = lower_bound R )