theorem Th4: :: PAPPUS:4

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 being Element of PCPP st c2 <> c1 & c3 <> c1 & c3 <> c2 & c4 <> c2 & c4 <> c3 & c5 <> c1 & c6 <> c1 & c6 <> c5 & c7 <> c5 & c7 <> c6 & 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,c7,c2 are_collinear & not c4,c10,c3 are_collinear & not c4,c7,c3 are_collinear & not c4,c10,c2 are_collinear & not c4,c7,c5 are_collinear & not c4,c10,c8 are_collinear & not c4,c7,c8 are_collinear & not c4,c10,c5 are_collinear & not c4,c7,c9 are_collinear & not c4,c10,c6 are_collinear & not c4,c7,c6 are_collinear & not c4,c10,c9 are_collinear & not c7,c10,c5 are_collinear & not c7,c4,c6 are_collinear & not c7,c10,c9 are_collinear & not c7,c4,c3 are_collinear & not c7,c10,c3 are_collinear & not c7,c4,c9 are_collinear & not c7,c10,c2 are_collinear & not c7,c4,c8 are_collinear & not c10,c4,c2 are_collinear & not c10,c7,c6 are_collinear & not c10,c4,c6 are_collinear & not c10,c7,c2 are_collinear & not c10,c4,c5 are_collinear & not c10,c7,c3 are_collinear & not c10,c4,c3 are_collinear & not c10,c7,c5 are_collinear )