let PCPP be CollProjectiveSpace; :: thesis: for c1, c2, c4, c5, c6, c8 being Element of PCPP st c4 <> c2 & c6 <> c1 & not c1,c2,c5 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c4,c6,c8 are_collinear holds
c8 <> c2
let c1, c2, c4, c5, c6, c8 be Element of PCPP; :: thesis: ( c4 <> c2 & c6 <> c1 & not c1,c2,c5 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c4,c6,c8 are_collinear implies c8 <> c2 )
assume that
A1: not c4 = c2 and
A2: not c6 = c1 and
A3: not c1,c2,c5 are_collinear and
A4: c1,c2,c4 are_collinear and
A5: c1,c5,c6 are_collinear and
A6: c4,c6,c8 are_collinear and
A7: c8 = c2 ; :: thesis: contradiction

now :: thesis: ( not c6,c1,c2 are_collinear & ( for v3, v2 being Element of PCPP holds
( c4 = c2 or not c2,c4,v2 are_collinear or not c2,c4,v3 are_collinear or v2,v3,c2 are_collinear ) ) & c2,c4,c6 are_collinear & c2,c4,c1 are_collinear )

( c6,c1,c1 are_collinear & c6,c1,c5 are_collinear ) by COLLSP:2, A5, HESSENBE:1;
hence not c6,c1,c2 are_collinear by A2, COLLSP:3, A3; :: thesis: ( ( for v3, v2 being Element of PCPP holds
( c4 = c2 or not c2,c4,v2 are_collinear or not c2,c4,v3 are_collinear or v2,v3,c2 are_collinear ) ) & c2,c4,c6 are_collinear & c2,c4,c1 are_collinear )
for v102, v103, v100, v104 being Element of PCPP holds
( v100 = v104 or not v104,v100,v102 are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104 are_collinear )

proof

let v102, v103, v100, v104 be Element of PCPP; :: thesis: ( v100 = v104 or not v104,v100,v102 are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104 are_collinear )
v104,v100,v104 are_collinear by COLLSP:5;
hence ( v100 = v104 or not v104,v100,v102 are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104 are_collinear ) by COLLSP:3; :: thesis: verum

end;

hence for v3, v2 being Element of PCPP holds
( c4 = c2 or not c2,c4,v2 are_collinear or not c2,c4,v3 are_collinear or v2,v3,c2 are_collinear ) ; :: thesis: ( c2,c4,c6 are_collinear & c2,c4,c1 are_collinear )
thus c2,c4,c6 are_collinear by A6, A7, HESSENBE:1; :: thesis: c2,c4,c1 are_collinear
thus c2,c4,c1 are_collinear by A4, COLLSP:8; :: thesis: verum

end;

hence contradiction by A1; :: thesis: verum