Existence of the Infimum of a Nonempty Subset of $\mathbb{R}$ Bounded Below

Let $\mathbb{R}$ denote the real numbers, whose order $\le$ is that of an ordered field and in particular a total order. Let $S\subseteq\mathbb{R}$ be nonempty and bounded below.

Then $S$ has a greatest lower bound in $\mathbb{R}$. By Uniqueness of the Supremum and of the Infimum it is unique, and is denoted $\inf S$.