Let(A = [-x1,0], B = [x1,0], C = [x2,x3], D = [x4,x5], P = [x4,0],
    Q = [x6,x7], R = [x8,x9]):
Simson := Theorem(
          [arbitrary(A,B,C), oncircle(A,B,C,D), perpfoot(D,P,A,B,P), 
           perpfoot(D,Q,A,C,Q), perpfoot(D,R,B,C,R)], 
           collinear(P,Q,R), [x5, x6, x7, x8, x9] );