This demo displays a sphere and a curve on the sphere.

The length of the curve is given in a readout in the control window.

Changin the value of t0 moves the point P on the curve, and point Q is a distance from P along the curve determined by u0. This distance from Q to P along the curve is given by the second readout. The distance from P to Q along the curve is given by the third readout. A midpoint between P and Q, M, is displayed on the sphere, as well as a red equator for which M is the north pole.

The checkbox X(u) displays the curve from Q to P, and the variable alpha will rotate the curve from P to Q about the vector determined by M.

According to Horn's Lemma, if the length of the curve is less than 2π, we can find a hemisphere such that the curve lies entirely within that.

This demo illustrates the idea of the proof in the following way. For any t0, we can find a u0 such that P and Q are exactly half way around the curve from each other. Thus, with X(u) turned off, we are looking at a curve of at most lenght π. If any portion of the curve intersects the red equator, when changing the value of alpha to 0 to rotate the other half curve, the other half curve will intersect the equator at an antipodal point. The distance between any two antipodal points is at least π, thus the lenght of the entire curve must be at least 2π. Therefore the curve of lenght less than 2π will not intersect the equator.