theorem Th12: :: PAPPUS:12

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5 being Element of PCPP st not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c2,c4 are_collinear holds
c2,c3,c4 are_collinear