theorem Th19: :: PAPPUS:19

for c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 being Element of (ProjectiveSpace (TOP-REAL 3)) st c1 <> c2 & c1 <> c3 & c2 <> c3 & c2 <> c4 & c3 <> c4 & c1 <> c5 & c1 <> c6 & c5 <> c6 & c5 <> c7 & c6 <> c7 & not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c4,c6,c9 are_collinear & c3,c7,c9 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear holds
( not c4,c2,c7 are_collinear & not c4,c3,c7 are_collinear & not c2,c3,c7 are_collinear & not c4,c2,c5 are_collinear & not c4,c2,c6 are_collinear & not c4,c3,c5 are_collinear & not c4,c3,c6 are_collinear & not c2,c7,c5 are_collinear & not c2,c7,c6 are_collinear & not c3,c7,c5 are_collinear & not c3,c7,c6 are_collinear & not c2,c3,c5 are_collinear & not c2,c3,c6 are_collinear & not c7,c5,c4 are_collinear & not c7,c6,c4 are_collinear & not c5,c6,c4 are_collinear & not c5,c6,c2 are_collinear & c4,c5,c8 are_collinear & c4,c6,c9 are_collinear & c2,c7,c8 are_collinear & c2,c6,c10 are_collinear & c3,c7,c9 are_collinear & c3,c5,c10 are_collinear )