# Ex215 in Chou (1988)
Let(A=[0,0], B=[u1,0], C=[u2,u3], H=[u2,x1], O=[x3,x2], A1=[x5,x4],
    B1=[x7,x6]):
Chou215 := Theorem(
    [not collinear(A,B,C), perpendicular(H,C,A,B), perpendicular(H,A,B,C),
     circumcenter(A,B,C,O), circumcenter(B,C,H,A1), circumcenter(A,C,H,B1)],
    concurrent(A,A1,B,B1,O,H), [x1,x2,x3,x4,x5,x6,x7]);

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