for PCPP being CollProjectiveSpace
for a1, a2, a3, c1, c3, x being Element of PCPP st not a1,a2,a3 are_collinear & a1,a2,c3 are_collinear & a2,a3,c1 are_collinear & c1,c3,x are_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 holds
( a1 <> x & a3 <> x )