Proof of The Nonnegative Bounds of a Bounded Linear Functional Have an Infimum, Which Is a Bound

Throughout, membership in $B_{F}$ is read off from Bounded Linear Functionals and the Dual Space of a Real Normed Space (ii): a real $C$ lies in $B_{F}$ exactly when $C\ge0$ and $|F(x)|\le C\lVert x\rVert$ for every $x\in X$.

Since $F\in X^{*}$, Bounded Linear Functionals and the Dual Space of a Real Normed Space (iv) and Bounded Linear Functionals and the Dual Space of a Real Normed Space (iii) provide a bound $C$ of $F$ in the sense of Bounded Linear Functionals and the Dual Space of a Real Normed Space (i), so that $|F(x)|\le C\lVert x\rVert$ for every $x\in X$. If $C\ge0$, then $C\in B_{F}$. If $C<0$, then, as $\lVert x\rVert\ge0$ by Norms and Real Normed Spaces (i),

$$|F(x)|\le C\lVert x\rVert\le0=0\cdot\lVert x\rVert\qquad\text{for every }x\in X,$$

so $0\in B_{F}$. In either case $B_{F}$ is nonempty.

Every element of $B_{F}$ is nonnegative, so $0$ is a lower bound of $B_{F}$. Hence the nonempty set $B_{F}$ has an infimum by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (viii), and $\inf B_{F}\ge0$ because the infimum is the greatest lower bound (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)). This proves (i).

It remains to show that $\inf B_{F}$ is itself a bound. Fix $x\in X$ and a real number $\eta>0$, and then put $\varepsilon=\eta/(\lVert x\rVert+1)>0$. Since $\inf B_{F}+\varepsilon$ exceeds the greatest lower bound of $B_{F}$, it is not a lower bound, so there is $C\in B_{F}$ with $C<\inf B_{F}+\varepsilon$. Then

$$|F(x)|\le C\lVert x\rVert\le(\inf B_{F}+\varepsilon)\lVert x\rVert\le(\inf B_{F})\lVert x\rVert+\eta .$$

As $\eta>0$ was arbitrary, $|F(x)|\le(\inf B_{F})\lVert x\rVert$. Together with $\inf B_{F}\ge0$ this says $\inf B_{F}\in B_{F}$, which is (ii).