theorem Th11: :: PAPPUS:11

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