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 eighth-degree polynomials satisfied by 
and 
are identical, proving that 
.
