One of the first exercises in J.L. Bell's A Primer of Infinitesimal Analysis asks the reader to show that, for arbitrary real numbers $a$, $b$, and $x$, if $a < b$, then either $x > a$ or $x < b$.
The reason this is not entirely trivial is that we're working in a constructive setting, one in which the law of the excluded middle does not hold. The goal is to prove the statement above from the axioms governing the strict ordering relation:
- $a < b$ and $b <c$ implies $a < c$
- $(a < a)$ is false
- $a < b$ implies $a + c < b + c$
- $a < b$ and $c > 0$ implies $ac < bc$
- either $0 < a$ or $a < 1$
- $a \neq b$ implies $a < b$ or $b < a$
Note that without the law of the excluded middle, we cannot establish the classical trichotomy that, for any two real numbers $x$ and $y$, one of $x < y$, $x = y$, or $x > y$ is true: it may still be the case that we cannot distinguish $x$ from $y$ sufficiently to establish any of these relations.
In Bell's presentation, we also know at this point that the real numbers with the operations of addition and multiplication form a field in the usual way, though with the caveat that in order to assume $x$ has a multiplicitive inverse we must know $x \neq 0$, a condition that is not automatic for numbers other than zero since we can't appeal to the law of the excluded middle.
Some Googling tells me that the statement to be proved is sometimes presented as a axiom (called co-transitivity) of constructive order relations. How can it be proved from Bell's axioms?
As a rule of thumb, in constructive mathematics often the way you prove a formula involving a disjunction is to start with an axiom which already has a disjunction. In this case notice that the only axioms mentioning disjunctions are 5 and 6. Also note that axiom 5 is kind of similar to what we have to prove, so that's the one we're going to use. It just needs a bit of adjusting.
First of all see that since $a < b$ we can apply axiom 3 to show that $0 < b - a$, so in particular we can divide by $b - a$.
Let $x' = \frac{x - a}{b - a}$. Now applying axiom 5 we know that either $0 < x'$ or $x' < 1$.
Suppose that $0 < x'$. Then by axiom 4 we can multiply through by $b - a$ (recall $0 < b - a$) to get $0 < x - a$, and then get $a < x$ by axiom 3.
Now suppose that $x' < 1$. Then multiplying through by $b - a$ again this time gives $x - a < b - a$. Then apply axiom 3 to get $x < b$.
But now we've shown that either $a < x$ or $x < b$ as required.