`` := Let(A = [-x1, 0],B = [x1, 0],C = [x2, x3],D = [x4, x5],P = [x4, 0],Q = [
x6, x7],R = [x8, x9]);
SimsonT := 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
]);
