# Feuerbach Theorem
Feuerbach := Theorem(
   [(x1^2-x2^2)*x5+2*x1*x2*(x2-x4), (x1^2-x3^2)*x5+2*x1*x3*(x3-x4),
    numer((x6-(x2+x4)/2)^2-(x6-(x3+x4)/2)^2),
    numer(x8^2-(x6-(x2+x4)/2)^2-(x7-x5/2)^2),
    4*x8^2-(2*x6-x2-x3)^2-4*x7^2, x9^2-x6^2-(x7-x1)^2],
   x9^4+x8^4+x1^4-2*x9^2*x8^2-2*x9^2*x1^2-2*x8^2*x1^2, [x4,x5,x6,x7,x8,x9]);

Remark(
`   See                                                               `,
`W.-t. Wu: Mechanical Theorem Proving in Geometries: Basic Principles.`,
`   Springer, Wien New York (1994).`
):
