theorem Th35:
for
P1,
P2,
P3,
P4,
P5,
P6,
P7,
P8,
P9 being
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) &
P1,
P2,
P3 are_collinear &
P1,
P2,
P3,
P4,
P5,
P6,
P7,
P8,
P9 are_in_Pascal_configuration holds
P7,
P8,
P9 are_collinear