**Proof**

If C = A or B, then the result is clear.
Suppose that C lies between A and B.

Observe that, by **D4** the value of d is invariant under

hyperbolic transformations. Thus we may transform the figure

to simplify the calculations.

By the Origin Lemma, there is an h-inversion **k** mapping C to O.

Suppose that **k** maps A to A' and B to B'

between A and B, O lies between A' and B'.

Let **H** be the h-line bisecting the angle between OA' and

the *positive* real axis, and let **h** denote h-inversion in **H**.

As O is on **H**, **h** fixes O. By our choice of **H**, **h** maps A'

to A" on the positive real axis. Suppose that **h** maps B' to B".

Then **t** = **h**o**k** maps C to O, A to A" and B to B".

As C lies between A and B, O lies between A" and B", so that

B" lies on the *negative* real axis.

Let A", B" have coordinates a and b, so -1 < b < 0 < a < 1.

Then

D(a,0) = |a| = a, so d(A",0) = 2arctanh(a),

D(b,0) = |b| = -b, so d(0,B") = d(B",0) = 2arctanh(-b),

D(a,b) = |a-b|/|b*a-1| = (a-b)/(1-ab) (as a > 0 and -b > 0),

so d(a,b) = 2 arctanh((a-b)/(1-ab)).

tanh(d(a,0)/2 + d(0,b)/2)

= tanh(arcanh(a) + arctanh(-b))

= (a+(-b))/(1 + a(-b))

= (a-b)/(1-ab)

= tanh(d(a,b)/2).

Thus, as tanh is a bijection,

d(a,0) + d(0,b) = d(a,b).

Since **t** does not alter the value of d,

d(A,B) = D(A,C) + D(C,B).