theorem Th5: :: PAPPUS:5

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