Accumulation below an unattained supremum (source code)

= Accumulation below an unattained supremum

If a nonempty real set $A$ has finite <supremum> $s$ and $s\notin A$, then every interval $(s-\varepsilon,s)$ contains infinitely many elements of $A$. Otherwise its finitely many elements have a largest value $m<s$; all remaining elements are at most $s-\varepsilon$, making $\max(m,s-\varepsilon)<s$ an <upper bound>. The interval cannot be empty either, by the defining approximation property of a <supremum>. Thus failure to attain a finite <supremum> forces accumulation from below.