theorem Th31: :: PASCAL:31

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