# Butterfly Theorem
Let(H = [0,0], O = [0,x1], P = [-x2,0], Q = [x2,0], A = [x3,x4], 
    B = [x5,x6], C = [x7,x8], D = [x9,x10], E = [x11,0], F = [x12,0]):
ButterflyA := Theorem(
    [arbitrary(H,O,P), midpoint(P,Q,H), circumcenter(P,Q,A,O), 
     online(A,H,B), oncircle(P,Q,A,B), oncircle(P,Q,A,C), 
     online(C,H,D), oncircle(P,Q,C,D), online(A,C,E), 
     online(B,D,F), not equal(A,B), not equal(C,D)],
    [midpoint(E,F,H)], [x4, x5, x6, x8, x9, x10, x11, x12] );
