proof verification - If $A$ is an ordered set has the Least upper bound property iff it has the greatest lower bound property.

Mentioned as an easy exercise in 'Topology', James R. Munkres, 2e, Pearson[page No:25]

If $A$ is an ordered set has the Least upper bound property iff it has the greatest
lower bound property.

An ordered set $A$ is said to have the least upper bound property if every nonempty subset $A_0$ of $A$ that is bounded above has least upper bound. $A$ satisfies this property. Suppose $B_0$ is an arbitrary set having lower bound. We need to prove it has the greatest lower bound. Suppose $L\subset A$ is the set of all lower bounds of the set $B_0$. $$\exists b_0\in B_0, \forall x\in L, x\leq b_0. $$
So, $L$ is bounded above. Hence, It has least upper bound. Let $b$ be the least upper bound of $L$. $$ \forall x\in L, x\leq b. $$ If $\exists b'\in B_0, b'\leq b,$ which contradict the fact that $b$ is the least upper bound of $L$. Hence,$$b\leq y, \forall y\in B_0.$$ So, $b$ is the lower bound. No element of $y\in L$ satisfy $ b\leq y$. Hence $b$ is the greatest lower bound. If this proof is correct, I can use the similar argument for the converse. I request you to verify my proof.

Answer

The idea is correct, but could be written down more clearly:

Let $A$ be an ordered set that satisfies the lub property.
Then $A$ satisfies the glb property:

Let $B$ be a non-empty subset of $A$ that is bounded below, define

$$L(B) = \{x \in A: \forall b \in B: x \le b\}$$ which is the set of lower bounds for $B$, which is by assumption non-empty.

Then for any fixed $b_0 \in B$ ($B$ is non-empty), and any $l \in L(B)$ we have $l \le b_0$. But this says that $L(B)$ is bounded above. So the lub property says that $l_0 = \operatorname{lub}(L(B))$ exists. Claim: $l_0 = \operatorname{glb}(B)$.

For this we need to show two things: $l_0$ is a lower bound for $B$ and there is no greater lower bound for $B$.

So let $b \in B$. Then, as before, $b$ as before is an upper bound for $L(B)$ by the definition of $L(B)$, and as $l_0$ is the least upper bound for $L(B)$ we have $l_0 \le b$. As $b$ was arbitary, $l_0$ is a lower bound for $B$.

Now suppose $m$ is any lower bound for $B$. Then again by definition, $m \in L(B)$.

As $l_0$ is the least upper bound for $L(B)$, it is an upperbound for $L(B)$ so $m \le l_0$. So all lower bounds for $B$ are below $l_0$.

Together this says that $l_0 = \operatorname{glb}(B)$ and so $A$ satisfies the glb-property.

The reverse is indeed similar: $\operatorname{lub}(B) = \operatorname{glb}(U(B))$, where $U(B)$ is the set of upperbounds for $B$.