# Pascal-Conic Theorem
PascalConic := Theorem(
    [x1*x6**2+x2*x6*x7+x3*x7**2+x4*x6+x5*x7+1, x3*x8**2+x5*x8+1, 
     x3*x8+x3*x9+x5, x6*x8+x7*x10-x8*x10, x1*x11**2+x4*x11+1, 
     x1*x11+x1*x12+x4, -x6*x13-x7*x12+x12*x13, 
     x1*x14**2+x2*x14*x15+x3*x15**2+x4*x14+x5*x15+1, 
     -x6*x12*x15+x6*x8*x12-x6*x8*x16-x7*x12*x16+x7*x12*x14-x8*x12*x14
        +x8*x14*x16+x12*x15*x16, 
     x8*x12-x12*x17-x8*x16, x11*x15-x11*x18+x14*x18, 
     x6*x10*x15+x6*x18*x19-x6*x10*x18+x7*x10*x19-x7*x10*x14-x14*x18*x19
        +x10*x14*x18-x10*x15*x19, 
     x18*x19-x10*x18+x10*x20, x9*x21-x9*x14-x15*x21, 
     -x6*x11*x15+x6*x9*x11-x6*x9*x22-x7*x11*x22+x7*x11*x14-x9*x11*x14
        +x9*x14*x22+x11*x15*x22, 
     x9*x11-x11*x23-x9*x22, x13*x22+x23*x24-x13*x24, x17*x21-x21*x25+x16*x25],
    -x19*x25-x20*x24+x24*x25,
    [x7,x8,x9,x10,x11,x12,x13,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25]);
