theorem Th13: :: PAPPUS:13

for PCPP being CollProjectiveSpace
for c1, c2, c5, c6, c7 being Element of PCPP st not c1,c2,c5 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear holds
c5,c6,c7 are_collinear