# Apollonian Circle Theorem

Let(O = [0,0], A = [x1,0], B = [x2, 0], H = [0, x3], P = [0,x4], Q = [0, x5],
    C = [x6,x7], D = [x8,x9], E = [x10,x11], F = [x12, 0], A1 = [x13,x14],
    B1 = [x15,x16], C1 = [x17,0], L = [x18,x19]):
ApollonCircle := Theorem(
   [equiangle(O,A,H,H,A,P), equiangle(O,B,H,H,B,Q), online(A,P,C), 
    online(B,Q,C), online(B,Q,D), online(A,H,D), online(A,P,E), 
    online(B,H,E), online(C,H,F), perpendicular(A,A1,A,H), online(B,Q,A1), 
    perpendicular(B,B1,B,H), online(A,P,B1), perpendicular(C,C1,C,H), 
    perpendicular(L,A1,L,D), perpendicular(L,C1,L,F)], perpendicular(L,B1,L,E),
   [x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19]);

Remark(
`   See`,
`S.-C. Chou: Mechanical Geometry Theorem Proving. D. Reidel, Dordrecht (1988)`,
`   [Example 453].`,
`D. Wang: Mechanical Approach for Polynomial Set and Its Related Fields. Ph.D`,
`   thesis, Academia Sinica (1987) [Section 2.4, Example 2].`
):
