let PCPP be CollProjectiveSpace; :: thesis: for c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 being Element of PCPP st not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c4,c6,c9 are_collinear & c3,c7,c9 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear holds
( c4,c2,c3 are_collinear & c4,c5,c8 are_collinear & c4,c9,c6 are_collinear & c7,c5,c6 are_collinear & c7,c9,c3 are_collinear & c7,c2,c8 are_collinear & c10,c2,c6 are_collinear & c10,c5,c3 are_collinear )
let c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 be Element of PCPP; :: thesis: ( not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c4,c6,c9 are_collinear & c3,c7,c9 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear implies ( c4,c2,c3 are_collinear & c4,c5,c8 are_collinear & c4,c9,c6 are_collinear & c7,c5,c6 are_collinear & c7,c9,c3 are_collinear & c7,c2,c8 are_collinear & c10,c2,c6 are_collinear & c10,c5,c3 are_collinear ) )
assume that
A1: not c1,c4,c7 are_collinear and
A2: c1,c4,c2 are_collinear and
A3: c1,c4,c3 are_collinear and
A4: c1,c7,c5 are_collinear and
A5: c1,c7,c6 are_collinear and
A6: c4,c5,c8 are_collinear and
A7: c7,c2,c8 are_collinear and
A8: c4,c6,c9 are_collinear and
A9: c3,c7,c9 are_collinear and
A10: c2,c6,c10 are_collinear and
A11: c3,c5,c10 are_collinear ; :: thesis: ( c4,c2,c3 are_collinear & c4,c5,c8 are_collinear & c4,c9,c6 are_collinear & c7,c5,c6 are_collinear & c7,c9,c3 are_collinear & c7,c2,c8 are_collinear & c10,c2,c6 are_collinear & c10,c5,c3 are_collinear )
( not c7 = c1 & not c4 = c1 & c1,c4,c4 are_collinear & c1,c7,c7 are_collinear ) by A1, COLLSP:2;
hence ( c4,c2,c3 are_collinear & c4,c5,c8 are_collinear & c4,c9,c6 are_collinear & c7,c5,c6 are_collinear & c7,c9,c3 are_collinear & c7,c2,c8 are_collinear & c10,c2,c6 are_collinear & c10,c5,c3 are_collinear ) by A2, COLLSP:3, A3, A11, HESSENBE:1, A10, A9, A8, A7, A6, A4, A5; :: thesis: verum