let PCPP be CollProjectiveSpace; :: thesis: for c1, c2, c4, c5, c6, c8 being Element of PCPP st c4 <> c1 & c6 <> c5 & not c1,c2,c5 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c4,c6,c8 are_collinear holds
c8 <> c5
let c1, c2, c4, c5, c6, c8 be Element of PCPP; :: thesis: ( c4 <> c1 & c6 <> c5 & not c1,c2,c5 are_collinear & c1,c2,c4 are_collinear & c1,c5,c6 are_collinear & c4,c6,c8 are_collinear implies c8 <> c5 )
assume that
A1: not c4 = c1 and
A2: not c6 = c5 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 = c5 ; :: thesis: contradiction

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

thus not c5,c1,c2 are_collinear by COLLSP:8, A3; :: thesis: ( c5,c4,c6 are_collinear & ( for v0 being Element of PCPP holds
( not c4,c1,v0 are_collinear or v0,c1,c2 are_collinear ) ) & ( not c5,c6,c4 are_collinear or c4,c1,c5 are_collinear ) )
thus c5,c4,c6 are_collinear by A6, A7, HESSENBE:1; :: thesis: ( ( for v0 being Element of PCPP holds
( not c4,c1,v0 are_collinear or v0,c1,c2 are_collinear ) ) & ( not c5,c6,c4 are_collinear or c4,c1,c5 are_collinear ) )
( c4,c1,c1 are_collinear & c4,c1,c2 are_collinear ) by A4, COLLSP:2, HESSENBE:1;
hence for v0 being Element of PCPP holds
( not c4,c1,v0 are_collinear or v0,c1,c2 are_collinear ) by A1, COLLSP:3; :: thesis: ( not c5,c6,c4 are_collinear or c4,c1,c5 are_collinear )

now :: thesis: ( ( 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 ) ) & c5,c6,c1 are_collinear )

thus 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 ) :: thesis: c5,c6,c1 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:2;
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;

thus c5,c6,c1 are_collinear by A5, COLLSP:8; :: thesis: verum

end;

hence ( not c5,c6,c4 are_collinear or c4,c1,c5 are_collinear ) by A2; :: thesis: verum

end;

hence contradiction by COLLSP:4; :: thesis: verum