@johnmangual. Two references are Introduction to Möbius Differential Geometry by Hertrich-Jeromin and Lie Sphere Geometry by Cecil. Personally, I prefer oriented circles and allow Mobius transformations to reverse the orientation, then the answer of Bryant is good enough.

are you sure about this "$\mathbb{C}\times S^1$"?

We also call it "de Sitter space".

@NoahS Yes, it's arbitrarily high. See arxiv.org/abs/math/0106095 . So it is known that they are not the same.

@NoahS, This could be arbitrarily high, isn't it?

@IgorRivin. Sorry, just revised the list. Which of Andreev's should I put?

@AndyPutman. The theorem itself is not purely graph theoretical. It is the area of discrete geometry or geometric graph theory. In my answer, the three variational principle proofs and the complete version by Brightwell and Scheinermann should be count as contributions from discrete geometors and graph theorists.

@Rob. I'm fully aware of its twin. What I missed in domotrop's proof is that this twin must be in the first quadrant, then the proof works by replacing $y$ by $x$ when constructing the parallelogram.

@domotrop. Thank you for explanation. So I imagine that you repeat the same argument to the part of the first quadrant above $\ell$, but replace $y$ by $x$ when constructing the parallelogram. This then covers all the angles. That's also why you can suppose $P$ is below $\ell$ wlog. Then I think the detail that bothers me is "$P$ minimizes the angle", which is actually the "angle" from below. I'm now totally OK with the proof.