# Thebault Theorem (Yang & Zhang, 1992)
Thebault := Theorem(
    [4*x1^2*u1^2*u2^4+6*u1^2*u2^4-2*u2^2-2*u2^6-2*u2^2*u1^4-2*u2^6
     *u1^4+u1^2+u1^2*u2^8+4*u2^4*u3-4*u2^4*u1^4*u3-4*u2^4*u3^2*u1^2,
     (4*u2^4-8*u2^4*u3*u1^2-4*u1^4*u2^4+8*x1*u1^2*u2^4)*x2^2+(-4*
     u2^2*u1^4+8*u2^4+4*u1^2-4*u2^6*u1^4-4*u2^6+8*u1^4*u2^4+4*u1^2*
     u2^8+8*u1^2*u2^4-8*u1^2*u2^2-4*u2^2-8*u2^6*u1^2)*x2+(-2*u1^2+4*
     u1^2*u2^4-2*u1^2*u2^8)*x1-1-8*u2^4*u3+8*u2^2*u3*u1^2+u1^4+2*
     u2^4+4*u2^6*u1^4*u3+4*u1^4*u3*u2^2-12*u2^4*u3*u1^2-2*u1^4*u2^4
     -2*u2^8*u3*u1^2-8*u2^4*u1^4*u3-2*u3*u1^2+u1^4*u2^8+4*u3*u2^2
     -u2^8+8*u2^6*u3*u1^2+4*u2^6*u3,
     (4*u2^4-4*u1^4*u2^4-8*u2^4*u3*u1^2-8*x1*u1^2*u2^4)*x3^2+(8*
     u1^4*u2^4+4*u1^2-4*u2^2*u1^4-8*u1^2*u2^2-4*u2^6*u1^4+8*u1^2*u2^4
     -8*u2^6*u1^2+4*u1^2*u2^8-4*u2^2+8*u2^4-4*u2^6)*x3+(2*u1^2-4*u1^2
     *u2^4+2*u1^2*u2^8)*x1-1+8*u2^2*u3*u1^2+8*u2^6*u3*u1^2+u1^4+2*u2^4
     -u2^8+4*u3*u2^2-12*u2^4*u3*u1^2-2*u1^4*u2^4-8*u2^4*u3-8*u2^4*
     u1^4*u3-2*u3*u1^2+u1^4*u2^8+4*u1^4*u3*u2^2+4*u2^6*u3+4*u2^6*
     u1^4*u3-2*u2^8*u3*u1^2,  
     x4*u1*u2+1-u1^2*u2^2, x5*u1*u2-u1^2+u2^2,
     (2*u1^2-2*u1^2*u2^4+2*x4*u1^2*u2^2+2*x5*u1^2*u2^2)*x6+(-u1^2
     -u1^2*u2^4)*x5+(-u1^2-u1^2*u2^4)*x4-u1^4+u2^4-1+u1^4*u2^4,
     (-u2^2+u1^2*u2^4-u2^2*u1^4+u1^2)*x7+(u2^2-u2^2*u1^4-u1^2+u1^2
     *u2^4-2*x5*u1^2*u2^2)*x6+(u1^2*u2^4+u1^2)*x5-u2^4+u1^4],
    (4*x2*u2^4+4*x3*u2^4)*x7+(-4*u2^2-4*u2^6+8*u2^4)*x6-4*u2^2-4*
     u2^6+1+6*u2^4-4*x2*x3*u2^4+u2^8, [x1,x2,x3,x4,x5,x6,x7]);
