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?