# EX401 in Chou (1988)
Let(o=[0,0], a=[u1,0], h=[u2,0], b=[u3,0], p=[x1,u4], c=[x2,u5],
    d=[x3,u6], e=[x5,x4], f=[x7,x6]):
Chou401 := Theorem(
    [sdistance(p,o)-sdistance(p,h)-(sdistance(o,a)-sdistance(h,b)),
     equidistance(c,o,o,a), equidistance(d,h,h,b),
     equidistance(e,o,o,a), equidistance(f,h,h,b),
     collinear(e,p,c), collinear(f,p,d)], cocircular(c,e,d,f),
    [x1,x2,x3,x4,x5,x6,x7]);

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