theorem Th33:
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) & 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 holds
P7,
P8,
P9 are_collinear