# Pascal Theorem
Pascal := Theorem(
          [2*x2*x8+2*x3*x7-x3^2-x2^2, 2*x1*x8-x1^2,
           -x9^2+2*x8*x9+2*x4*x7-x4^2, -x10^2+2*x8*x10+2*x5*x7-x5^2,
           -x11^2+2*x8*x11+2*x6*x7-x6^2, (x5-x4)*x12+x4*x10-x5*x9, 
           (x6-x5)*x14+(-x11+x10)*x13+x5*x11-x6*x10,
           x3*x14+(-x2+x1)*x13-x1*x3, -x6*x16+x11*x15,
           (x4-x3)*x16+(-x9+x2)*x15+x3*x9-x2*x4],
          -x13*x16+(x14-x12)*x15+x12*x13,
          [x7,x8,x9,x10,x11,x12,x13,x14,x15,x16]);
