Let(A = [-x1,0], B = [x1,0], C = [x2,x3], D = [x4,x5], A1 = [x6,x7],
    B1 = [x8,x9], C1 = [x10,x11]):
SimsonP := Theorem(
    [arbitrary(A,B,C), oncircle(A,B,C,D), oncircle(A,B,C,A1), 
     oncircle(A,B,C,B1), oncircle(A,B,C,C1), perpendicular(D,A1,B,C),
     perpendicular(D,B1,A,C), perpendicular(D,C1,B,A)],
    [parallel(A,A1,B,B1),parallel(A,A1,C,C1)], 
    [x5, x6, x7, x8, x9, x10, x11] );
