theorem Th15: :: PAPPUS:15

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