# Ex144 in Chou (1988)
Let(a=[-u1,0], b=[u1,0], c=[u2,u3], o=[0,x1], d=[u4,x2] ,e=[x3,x4],
    f=[x5,x6], g=[u4,0], e1=[x7,x8], f1=[x9,x10], g1=[x11,x12]):
Chou144 := Theorem(
    [equidistance(b,o,o,a), equidistance(c,o,o,a),
     equidistance(d,o,o,a), collinear(e,b,c),
     perpendicular(e,d,b,c), collinear(f,a,c),
     perpendicular(f,d,a,c), collinear(g,a,b),
     perpendicular(g,d,a,b), parallel(e1,d,a,o),
     perpendicular(e1,a,a,o), parallel(f1,d,b,o),
     perpendicular(f1,b,b,o), parallel(g1,d,c,o),
     perpendicular(g1,c,c,o)],
    sdistance(d,e)*sdistance(d,f)*sdistance(d,g)-sdistance(d,e1)*
    sdistance(d,f1)*sdistance(d,g1), ['cat(x,i)'$'i'=1..12]);

Remark(
`   See`,
`S.-C. Chou: Mechanical Geometry Theorem Proving. D. Reidel, Dordrecht (1988)`,
`   [Example 144].`
):
