Throughout we use the elementary order arithmetic of Elementary Order Arithmetic in an Ordered Field, whose clause numbers are cited explicitly.
1. (The real line.) R is an interval: the defining condition asks that yβR whenever x,zβR, yβR and xβ€yβ€z, which holds trivially.
By clause 6, 0<1, so 0ξ =1; hence R contains the two distinct points 0 and 1.
Let xβR. From 0<1 and clause 1 (strict compatibility with addition, adding x) we get x+0<x+1, that is, x<x+1. From 0<1 and clause 4 (sign reversal) we get β1<0, and adding x gives x+(β1)<x+0, that is, xβ1<x. Since xβ1,x+1βR and xβ1<x<x+1, the point x is an interior point of R.
2. (Closed subintervals.) Let u,vβI with uβ€v, and let yβ[u,v], so that uβ€yβ€v. Since u,vβI and I is an interval, yβI. Hence [u,v]βI.
3. (Points strictly between.) Let p,qβI with p<x<q. Then pβ€xβ€q, so xβI because I is an interval. Since p,qβI and p<x<q, the point x is an interior point of I by the definition of an interior point.
4. (Open intervals.) First, (p,q) is an interval. Let x,zβ(p,q) and let yβR with xβ€yβ€z. From p<x and xβ€y, clause 2 (mixed transitivity) gives p<y; from yβ€z and z<q, the same clause gives y<q. Hence yβ(p,q).
Now let xβ(p,q), so p<x<q. By clause 1, p<x gives 0<xβp, and x<q gives 0<qβx. By clause 8 (halving), 0<(xβp)β
2β1 and (xβp)β
2β1<xβp, and likewise 0<(qβx)β
2β1<qβx. Put
u=p+(xβp)β
2β1,v=x+(qβx)β
2β1.
Adding p to 0<(xβp)β
2β1<xβp and using clause 1 gives p<u<p+(xβp)=x. Adding x to 0<(qβx)β
2β1<qβx gives x<v<x+(qβx)=q. Hence p<u<x<v<q, so u,vβ(p,q) and u<x<v; therefore x is an interior point of (p,q).
5. (Closed intervals.) Let aβ€b. Then [a,b] is an interval: if x,zβ[a,b] and xβ€yβ€z, then aβ€xβ€y and yβ€zβ€b, so aβ€yβ€b and hence yβ[a,b].
Suppose moreover a<b. Then a,bβ[a,b] and aξ =b, so [a,b] contains at least two points. Finally, let xβ(a,b), so a<x<b; since a,bβ[a,b], claim 3 applied to the interval [a,b] shows that x is an interior point of [a,b].