Introduction:
The underline notation $\underline{x},\underline{\mathcal{M}},$ is just "decoration" used to distinguish symbols. The + sign applied to sets means
$$\mathcal{M}+\underline{\mathcal{M}}\equiv \left\{x+ \underline{x}\backepsilon x\in\mathcal{M}\land\underline{x}\in\underline{\mathcal{M}}\right\}.$$
The $\backepsilon,$ meaning such that, is a commonly used alternative for $\vert.$ So
$$\left\{x+ \underline{x}\backepsilon x\in\mathcal{M}\land\underline{x}\in\underline{\mathcal{M}}\right\}\equiv \left\{x+ \underline{x}\vert x\in\mathcal{M}\land\underline{x}\in\underline{\mathcal{M}}\right\}.$$
What follows addresses only part of a larger proof. A screen-scrape of an older version of the proof is at the bottom of this post. My question focuses on the first expression with a $\dagger$ next to it.
I begin with the proof, roughly as it is presented in BBFSK Pages 137-138. I then work progressively toward a modified version of the $\dagger$ statement which I believe to be more logically rigorous than the one appearing below.
Given some number set $\mathcal{M}$ we denote the set of upper bounds of $\mathcal{M}$ by $\mathcal{S}(\mathcal{M}).$ Next we define the set
$$\underline{\mathcal{M}}\equiv\left\{ \underline{x}\backepsilon-\underline{x}\in\mathcal{S}(\mathcal{M})\right\}.$$
Now we assume $z\in\mathcal{S}(\mathcal{M}+\underline{\mathcal{M}}).$ If $x\in\mathcal{M},$ and $\underline{x}\in\underline{\mathcal{M}}$ then $z\geq\underline{x}+x$, which means the same thing as $z-\underline{x}\in S(\mathcal{M}).$ This follows from the definition
$$\underline{x}\in\underline{\mathcal{M}}\iff-\underline{x}\in\mathcal{S}\left(\mathcal{M}\right)\iff\forall_{x\in\mathcal{M}}\left[-\underline{x}\ge x\right].$$
So
$$\left(\underline{x}\in\underline{\mathcal{M}}\land z\in\mathcal{S}\left(\mathcal{M}+\underline{\mathcal{M}}\right)\right) \iff\forall_{x\in\mathcal{M}}\left[z\ge x+\underline{x}\right] \iff\forall_{x\in\mathcal{M}}\left[z-\underline{x}\ge x\right].$$
That may be written as $z\geq\underline{x}+x\iff z-\underline{x}\in S(\mathcal{M}).$ So we have $$ \left(\left(x\in\mathcal{M}\land\underline{x}\in\underline{\mathcal{M}}\right)\implies z\geq\underline{x}+x\right) $$
$$ \land\left(\left(x\in\mathcal{M}\land\underline{x}\in\underline{\mathcal{M}}\right)\implies\left(z\geq\underline{x}+x\iff z-\underline{x}\in S(\mathcal{M})\right)\right). $$
We might state this as: for all $x\in\mathcal{M}$ and $\underline{x}\in\underline{\mathcal{M}}$ we have $z\geq\underline{x}+x,$ and $z\geq\underline{x}+x$ is equivalent to $z-\underline{x}\in S(\mathcal{M}).$ Or: for all $x\in\mathcal{M}$ and $\underline{x}\in\underline{\mathcal{M}}$ we have $z\geq\underline{x}+x\iff z-\underline{x}\in S(\mathcal{M}).$ So why not use quantifier notation and write:
$$ \forall_{x\in\mathcal{M},\underline{x}\in\underline{\mathcal{M}}}\left[z\geq\underline{x}+x\iff z-\underline{x}\in S(\mathcal{M})\right]? $$
In that form, it looked correct to me. But if we write the equivalent statement
$$ \left(x\in\mathcal{M}\land\underline{x}\in\underline{\mathcal{M}}\right)\implies\left(z\geq\underline{x}+x\iff z-\underline{x}\in S(\mathcal{M})\right). $$
It doesn't seem to have the intended meaning. This can be seen by comparing truth tables.
Let
$A:=z\geq\underline{x}+x;$$B:=z-\underline{x}\in S(\mathcal{M});$and $C:=x\in\mathcal{M}\land\underline{x}\in\underline{\mathcal{M}}.$
Then the truth table of $C\implies\left(A\iff B\right)$ is different from that of $\left(C\implies A\right)\land\left(C\implies\left(A\iff B\right)\right).$
So $$ \forall_{x\in\mathcal{M},\underline{x}\in\underline{\mathcal{M}}}\left[z\geq\underline{x}+x\iff z-\underline{x}\in S(\mathcal{M})\right] $$
doesn't mean the same thing as
$$ \forall_{x\in\mathcal{M},\underline{x}\in\underline{\mathcal{M}}}\left[z\geq\underline{x}+x\right]\land\left(z\geq\underline{x}+x\iff z-\underline{x}\in S(\mathcal{M})\right). $$
But $x$ and $\underline{x}$ aren't bound in the second term, so that really isn't the statement I want, either. A more accurate statement would seem to be
$$ \forall_{x\in\mathcal{M},\underline{x}\in\underline{\mathcal{M}}}\left[z\geq\underline{x}+x\right]\land\forall_{x\in\mathcal{M},\underline{x}\in\underline{\mathcal{M}}}\left[z\geq\underline{x}+x\iff z-\underline{x}\in S(\mathcal{M})\right]. $$
But then, what about
$$ \forall_{x\in\mathcal{M},\underline{x}\in\underline{\mathcal{M}}}\left[\left(z\geq\underline{x}+x\right)\land\left(z\geq\underline{x}+x\iff z-\underline{x}\in S(\mathcal{M})\right)\right]? $$
Are the last two statements equivalent? Does the last statement mean the same thing as my original natural language statement? That is: are $C\implies\left(A\land A\iff B\right)$ and $\left(C\implies A\right)\land\left(C\implies\left(A\iff B\right)\right)$ equivalent statements meaning the same thing as my original natural language sentence?
The following is the truth table I generated to show $$ \left(\left(C\implies A\right)\land\left(C\implies\left(A\iff B\right)\right)\right)\iff\left(C\implies\left(A\land A\iff B\right)\right). $$
This is a screen-scrape of the version in my notes with which I began. Note that I used $\overline{\mathcal{M}}$ instead of $\underline{\mathcal{M}}$. The statements are not intended to be rigorously correct. I was merely trying to capture my thought process.
When you express mathematical statements using propositional logic variables, you abstract away from the meaning of those statements. Thus, relationships that hold true in the original mathematical domain may no longer hold true in propositional logic.
For example, once we symbolize the mathematical statements $x>1$ and $x \leq 1$ as $A$ and $B$ respectively, it is no longer the case that exactly one of these statements is true. That is, when we do a truth-table analysis on $A$ and $B$, we find that there is a row where both are true, as well as a row where both are false, but obviously, as mathematical statements, neither of those can happen.
In other words, it is possible that your logical analysis does not match up with the mathematical analysis.
I suspect something like this is going on in your example, though my math skills aren't good enough to understand the reasoning you went through in your post.