Given two circles, draw the tangents from the center of each circle to the sides of the other. Then the line segments and are of equal length.
The theorem can be proved by brute force by setting up the nine equations
(1)
 
(2)
 
(3)
 
(4)
 
(5)
 
(6)
 
(7)
 
(8)
 
(9)

and using Gröbner basis to determine the polynomial equations satisfied by and while eliminate , , , , , , and . The resulting eighthdegree polynomials satisfied by and are identical, proving that .