theorem Th6: :: PAPPUS:6

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