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

In the setting of Separable Real Normed Spaces and Hahn–Banach: Notation, let $X$ be a real normed space, let $F\in X^{*}$ be an element of the dual space, and let $B_{F}$ be its set of nonnegative bounds.

(i) Existence. $B_{F}$ is nonempty and bounded below, with $0$ as a lower bound; hence it has an infimum, and $\inf B_{F}\ge0$.

(ii) The infimum is a bound. $\inf B_{F}\in B_{F}$, that is,

$$|F(x)|\le(\inf B_{F})\,\lVert x\rVert\qquad\text{for every }x\in X.$$