let P1, P2, P3, P4, P5, P6, P7, P8, P9 be Point of (ProjectiveSpace (TOP-REAL 3)); for a, b, c, d, e, f being Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & {P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & not P1,P2,P3 are_collinear & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration holds
P7,P8,P9 are_collinear
let a, b, c, d, e, f be Real; ( ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & {P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & not P1,P2,P3 are_collinear & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration implies P7,P8,P9 are_collinear )
assume that
A1:
( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 )
and
A2:
{P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f)
and
A3:
( not P1,P2,P3 are_collinear & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration )
; P7,P8,P9 are_collinear
( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not P7,P2,P5 are_collinear & not P1,P2,P5 are_collinear & not P1,P2,P6 are_collinear & not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear & not P1,P5,P7 are_collinear & not P2,P4,P5 are_collinear & not P2,P4,P6 are_collinear & not P2,P4,P7 are_collinear & not P2,P5,P9 are_collinear & not P2,P6,P8 are_collinear & not P2,P7,P8 are_collinear & not P2,P7,P9 are_collinear & not P3,P4,P5 are_collinear & not P3,P4,P6 are_collinear & not P3,P5,P8 are_collinear & not P3,P6,P8 are_collinear & not P5,P7,P8 are_collinear & not P5,P7,P9 are_collinear & P1,P5,P9 are_collinear & P1,P6,P8 are_collinear & P2,P4,P9 are_collinear & P2,P6,P7 are_collinear & P3,P4,P8 are_collinear & P3,P5,P7 are_collinear )
by A3, Th32;
hence
P7,P8,P9 are_collinear
by A1, A2, Th33; verum