let PCPP be CollProjectiveSpace; :: thesis: 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
let c2, c3, c4, c6, c8 be Element of PCPP; :: thesis: ( c4 <> c2 & c4 <> c3 & c8 <> c2 & not c2,c3,c6 are_collinear & c2,c3,c4 are_collinear & c2,c6,c8 are_collinear implies not c3,c4,c8 are_collinear )
assume that
A1: not c4 = c2 and
A2: not c4 = c3 and
A3: not c8 = c2 and
A4: not c2,c3,c6 are_collinear and
A5: c2,c3,c4 are_collinear and
A6: c2,c6,c8 are_collinear and
A7: c3,c4,c8 are_collinear ; :: thesis: contradiction

now :: thesis: ( c4,c2,c3 are_collinear & c3,c4,c2 are_collinear & c4,c2,c2 are_collinear & ( not c8,c2,c4 are_collinear or c4,c2,c6 are_collinear ) & c3,c4,c4 are_collinear )

thus c4,c2,c3 are_collinear by A5, HESSENBE:1; :: thesis: ( c3,c4,c2 are_collinear & c4,c2,c2 are_collinear & ( not c8,c2,c4 are_collinear or c4,c2,c6 are_collinear ) & c3,c4,c4 are_collinear )
thus c3,c4,c2 are_collinear by A5, COLLSP:8; :: thesis: ( c4,c2,c2 are_collinear & ( not c8,c2,c4 are_collinear or c4,c2,c6 are_collinear ) & c3,c4,c4 are_collinear )
thus c4,c2,c2 are_collinear by COLLSP:2; :: thesis: ( ( not c8,c2,c4 are_collinear or c4,c2,c6 are_collinear ) & c3,c4,c4 are_collinear )
( c8,c2,c2 are_collinear & c8,c2,c6 are_collinear ) by A6, HESSENBE:1, COLLSP:2;
hence ( ( not c8,c2,c4 are_collinear or c4,c2,c6 are_collinear ) & c3,c4,c4 are_collinear ) by A3, COLLSP:2, COLLSP:3; :: thesis: verum

end;

hence contradiction by A7, A1, A4, A2, COLLSP:3; :: thesis: verum