LPO $\forall x \in \mathbb{R} ( x = 0 \vee x < 0 \vee x > 0)$.
MP $ \forall x \in \mathbb{R} (\neg (x = 0) \Rightarrow \vert x \vert > 0)$.
LLPO $\forall x \in \mathbb{R} ( x \ge 0 \vee x \le 0)$.
I was told that in Bishop style constructive mathematics the following holds:
$LPO \Leftrightarrow MP+ LLPO$.
$\Rightarrow$ is easy to show, but I can't verify the other direction. When I looked it up, I only got a theorem
$LPO \Leftrightarrow MP+ WLPO$.
But $LLPO$ does not imply $WLPO$, so I am rather confused.