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 = hok 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).