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