# Butterfly Theorem
hyp := {-x5**2+x1**2+2*x4*x6-x6**2, 
-x2**2+x1**2+2*x3*x4-x3**2, -x7*x6-x1*x6+x5
*x8+x1*x8, -x3*x7+x3*x1+x2*x8-x1*x8, 2*x8-x11, 
2*x7-x10-x9, x7*(x7-x9)+(x8-x4)*x8}:
con := -x11*x2+x5*x11+x6*x2+x10*x3-x10*x6-x5*x3:
ord := [x4, x6, x7, x8, x9, x10, x11]:
Butterfly := Theorem(hyp,con,ord);
