Sup and Inf in R have sequences converging to them

Stream: Is there code for X?

[Keefer Rowan]

Is there theorem of the form $\forall E \subseteq \mathbb{R}, E \text{ bounded and nonempty } \to \exists \{a_n\} \subseteq E, a_n \longrightarrow \sup E$?

[Kevin Buzzard]

So we certainly have that E has a sup, but you might have to build the sequence by hand unless there's some trick with filters :-)

[Yury G. Kudryashov]

Do you want this sequence to be increasing?