Weak Archimedean property instead of Archimedean property

[Mohammad Tahmasbi]

I have written a proof that shows the decomposability of R^d (Dedekind real numbers) is equivalent to WLPO_R^d which states that for all x in R^d, either x=0 or ¬(x=0).

I wanted to rewrite the proof so that it also works for R^e. By R^e I mean classical real numbers, described by Troelstra and van Dalen in the book Constructivism in mathematics. I think R^e is also known as MacNeille real numbers in the literature. But there is a problem here. The problem is, R^e is not Archimedean. It is just weakly Archimedean which means

∀x∈R^e ¬¬∃n∈ℕ x<n.

But in my proof, I used the fact that R^d is Archimedean. I wanted to know that can we complete the proof, using weak Archimedean property instead of Archimedean property?

I explained the problem in details on mathoverflow. Please see the link below if you want to see the details:

https://mathoverflow.net/questions/480572/weak-archimedean-property-instead-of-archimedean-property

Do you have any idea that may help me with this problem?

Thank you very much for your help.