Completeness implies an infimum

Question

Let $F$ be an ordered field where every non-empty subset which is bounded above has a supremum. Prove that every non-empty subset which is bounded below has an infimum.

Let $S_1 = \{-x \mid x \in S\}$. Let $x_0$ be a lower bound of $S$, which means $x_0 \leq x$ for all $x \in S$. Then we have $-x_0 \geq -x$ for all $-x \in S_1$ so $-x_0$ is an upper bound for $S_1$. So $S_1$ is bounded above.

Let $-x_1$ be the supremum of $S_1$. We want to show that $x_1$ is the infimum of $S$.

First we show that $x_1$ is a lower bound of $S$. We know that since $-x_1$ is the supremum of $S_1$, $-x_1 \geq -x$ for all $-x \in S_1$. So $x_1 \leq x$ for all $x \in S$, so $x_1$ is a lower bound for $S$.

Next we show that if $x_2 \in F$ and $x_2 > x_1$, then $x_2$ is not a lower bound for $S$. If $x_2$ is a lower bound for $S$, then $x_2 \leq x$ for all $x \in S$. Then that means $-x_2 \geq -x$ for all $-x \in S_1$. So $-x_2$ is an upper bound for $S_1$. But we said that $x_2 > x_1$, so $-x_2 < -x_1$, which contradicts that $-x_1$ is the supremum of $S_1$. Since $x_2$ is not a lower bound for $S$, $x_1$ is the infimum.

Is this proof okay? If so, what can I improve on? If not, what should I change?

Answer 1

Your proof works fine, though it feels longer than it really needs to be. It seems like the key insight in your proof is that $f(x)=-x$ reverses the order of everything (i.e. if $a>b$ then $f(a)<f(b)$) and $f(f(x))=x$. Then, your proof could proceed as:

Let $S$ be a set with a lower bound. Notice that the image $f[S]$ has an upper bound and thus has a least upper bound (supremum) $x$ and that, since "least upper bound" is a property of the order dual to "greatest lower bound", the set $S=f[f[S]]$ must have $f(x)$ be its greatest lower bound and thus have

But, essentially, this is what your proof already does; it's just a matter of how much rigor you want to put in and whether this feels like it obscures the insight or feels like a helpful demonstration of why it holds. (Though the above argument of mine is not terribly far from a formal argument using duality)