for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5, c6, c7 being Element of PCPP st c3 <> c1 & c4 <> c1 & c4 <> c3 & c3 <> c2 & c4 <> c2 & c6 <> c1 & c7 <> c1 & c7 <> c6 & c6 <> c5 & c7 <> c5 & not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear holds
( not c1,c3,c6 are_collinear & c1,c3,c4 are_collinear & c1,c6,c7 are_collinear & c3 <> c1 & c2 <> c1 & c3 <> c2 & c4 <> c3 & c4 <> c2 & c6 <> c1 & c5 <> c1 & c6 <> c5 & c7 <> c6 & c7 <> c5 & not c1,c4,c7 are_collinear & c1,c4,c3 are_collinear & c1,c4,c2 are_collinear & c1,c7,c6 are_collinear & c1,c7,c5 are_collinear )