let PCPP be CollProjectiveSpace; :: thesis: for c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 being Element of PCPP st c2 <> c1 & c3 <> c1 & c3 <> c2 & c4 <> c2 & c4 <> c3 & c5 <> c1 & c6 <> c1 & c6 <> c5 & c7 <> c5 & c7 <> c6 & 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
( not c4,c7,c2 are_collinear & not c4,c10,c3 are_collinear & not c4,c7,c3 are_collinear & not c4,c10,c2 are_collinear & not c4,c7,c5 are_collinear & not c4,c10,c8 are_collinear & not c4,c7,c8 are_collinear & not c4,c10,c5 are_collinear & not c4,c7,c9 are_collinear & not c4,c10,c6 are_collinear & not c4,c7,c6 are_collinear & not c4,c10,c9 are_collinear & not c7,c10,c5 are_collinear & not c7,c4,c6 are_collinear & not c7,c10,c9 are_collinear & not c7,c4,c3 are_collinear & not c7,c10,c3 are_collinear & not c7,c4,c9 are_collinear & not c7,c10,c2 are_collinear & not c7,c4,c8 are_collinear & not c10,c4,c2 are_collinear & not c10,c7,c6 are_collinear & not c10,c4,c6 are_collinear & not c10,c7,c2 are_collinear & not c10,c4,c5 are_collinear & not c10,c7,c3 are_collinear & not c10,c4,c3 are_collinear & not c10,c7,c5 are_collinear )
let c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 be Element of PCPP; :: thesis: ( c2 <> c1 & c3 <> c1 & c3 <> c2 & c4 <> c2 & c4 <> c3 & c5 <> c1 & c6 <> c1 & c6 <> c5 & c7 <> c5 & c7 <> c6 & 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 ( not c4,c7,c2 are_collinear & not c4,c10,c3 are_collinear & not c4,c7,c3 are_collinear & not c4,c10,c2 are_collinear & not c4,c7,c5 are_collinear & not c4,c10,c8 are_collinear & not c4,c7,c8 are_collinear & not c4,c10,c5 are_collinear & not c4,c7,c9 are_collinear & not c4,c10,c6 are_collinear & not c4,c7,c6 are_collinear & not c4,c10,c9 are_collinear & not c7,c10,c5 are_collinear & not c7,c4,c6 are_collinear & not c7,c10,c9 are_collinear & not c7,c4,c3 are_collinear & not c7,c10,c3 are_collinear & not c7,c4,c9 are_collinear & not c7,c10,c2 are_collinear & not c7,c4,c8 are_collinear & not c10,c4,c2 are_collinear & not c10,c7,c6 are_collinear & not c10,c4,c6 are_collinear & not c10,c7,c2 are_collinear & not c10,c4,c5 are_collinear & not c10,c7,c3 are_collinear & not c10,c4,c3 are_collinear & not c10,c7,c5 are_collinear ) )
assume that
A1: not c2 = c1 and
A2: not c3 = c1 and
A3: not c3 = c2 and
A4: not c4 = c2 and
A5: not c4 = c3 and
A6: not c5 = c1 and
A7: not c6 = c1 and
A8: not c6 = c5 and
A9: not c7 = c5 and
A10: not c7 = c6 and
A11: not c1,c4,c7 are_collinear and
A12: c1,c4,c2 are_collinear and
A13: c1,c4,c3 are_collinear and
A14: c1,c7,c5 are_collinear and
A15: c1,c7,c6 are_collinear and
A16: c4,c5,c8 are_collinear and
A17: c7,c2,c8 are_collinear and
A18: c4,c6,c9 are_collinear and
A19: c3,c7,c9 are_collinear and
A20: c2,c6,c10 are_collinear and
A21: c3,c5,c10 are_collinear and
A22: ( c4,c7,c2 are_collinear or c4,c10,c3 are_collinear or c4,c7,c3 are_collinear or c4,c10,c2 are_collinear or c4,c7,c5 are_collinear or c4,c10,c8 are_collinear or c4,c7,c8 are_collinear or c4,c10,c5 are_collinear or c4,c7,c9 are_collinear or c4,c10,c6 are_collinear or c4,c7,c6 are_collinear or c4,c10,c9 are_collinear or c7,c10,c5 are_collinear or c7,c4,c6 are_collinear or c7,c10,c9 are_collinear or c7,c4,c3 are_collinear or c7,c10,c3 are_collinear or c7,c4,c9 are_collinear or c7,c10,c2 are_collinear or c7,c4,c8 are_collinear or c10,c4,c2 are_collinear or c10,c7,c6 are_collinear or c10,c4,c6 are_collinear or c10,c7,c2 are_collinear or c10,c4,c5 are_collinear or c10,c7,c3 are_collinear or c10,c4,c3 are_collinear or c10,c7,c5 are_collinear ) ; :: thesis: contradiction
A23: not c7 = c1 by COLLSP:2, A11;
A24: c4,c3,c1 are_collinear by A13, HESSENBE:1;
A25: c7,c5,c1 are_collinear by A14, HESSENBE:1;
A26: c1,c5,c7 are_collinear by A14, HESSENBE:1;
A27: c7,c6,c1 are_collinear by A15, HESSENBE:1;
A28: c1,c6,c7 are_collinear by A15, HESSENBE:1;
A29: 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: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;

A30: for v103, v104, v102, v101 being Element of PCPP holds
( v102 = v101 or not v101,v102,v103 are_collinear or not v101,v102,v104 are_collinear or v102,v103,v104 are_collinear )

proof

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

end;

A31: c2,c4,c1 are_collinear by A12, HESSENBE:1;
( c4,c2,c1 are_collinear & c4,c2,c4 are_collinear ) by COLLSP:2, A12, HESSENBE:1;
then A32: not c4,c2,c7 are_collinear by A4, COLLSP:3, A11;
( c1,c2,c1 are_collinear & c1,c2,c4 are_collinear ) by COLLSP:2, A12, HESSENBE:1;
then A33: not c1,c2,c7 are_collinear by A1, COLLSP:3, A11;
c4,c3,c4 are_collinear by COLLSP:2;
then A34: not c4,c3,c7 are_collinear by A24, A11, A5, COLLSP:3;
( c1,c3,c1 are_collinear & c1,c3,c4 are_collinear ) by COLLSP:2, A13, HESSENBE:1;
then A35: not c1,c3,c7 are_collinear by A2, COLLSP:3, A11;
c7,c5,c7 are_collinear by COLLSP:2;
then A36: not c7,c5,c4 are_collinear by A25, A9, COLLSP:3, A11;
c7,c5,c7 are_collinear by COLLSP:2;
then A37: not c7,c5,c2 are_collinear by A9, A25, COLLSP:3, A33;
A38: c1,c5,c1 are_collinear by COLLSP:2;
c7,c6,c7 are_collinear by COLLSP:2;
then A39: not c7,c6,c4 are_collinear by A10, COLLSP:3, A27, A11;
c7,c6,c7 are_collinear by COLLSP:2;
then A40: not c7,c6,c2 are_collinear by A27, A10, COLLSP:3, A33;
A41: c8,c4,c5 are_collinear by A16, HESSENBE:1;
A42: c9,c4,c6 are_collinear by A18, HESSENBE:1;
A43: c10,c2,c6 are_collinear by A20, HESSENBE:1;
A44: c10,c3,c5 are_collinear by A21, HESSENBE:1;
A45: c10,c5,c3 are_collinear by A21, HESSENBE:1;
( c3,c4,c4 are_collinear & c3,c4,c1 are_collinear ) by COLLSP:2, A13, HESSENBE:1;
then A46: ( not c3,c4,c5 are_collinear or c1,c5,c4 are_collinear ) by A5, COLLSP:3;
( c5,c7,c7 are_collinear & c5,c7,c1 are_collinear ) by COLLSP:2, A14, HESSENBE:1;
then A47: not c5,c7,c3 are_collinear by A35, A9, COLLSP:3;

now :: thesis: ( c2,c4,c4 are_collinear & not c1,c6,c4 are_collinear )

thus c2,c4,c4 are_collinear by COLLSP:2; :: thesis: not c1,c6,c4 are_collinear
c1,c6,c1 are_collinear by COLLSP:2;
hence not c1,c6,c4 are_collinear by A7, COLLSP:3, A28, A11; :: thesis: verum

end;

then A48: not c2,c4,c6 are_collinear by A4, COLLSP:3, A31;
A49: for v2, v101, v100 being Element of PCPP holds
( v101 = v100 or not v100,v101,v2 are_collinear or v2,v100,v101 are_collinear )

proof

let v2, v101, v100 be Element of PCPP; :: thesis: ( v101 = v100 or not v100,v101,v2 are_collinear or v2,v100,v101 are_collinear )
for v102, v104, v100, v103 being Element of PCPP holds
( v100 = v103 or not v103,v100,v102 are_collinear or not v103,v100,v104 are_collinear or v102,v103,v104 are_collinear )

proof

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

end;

then ( v101 = v100 or not v100,v101,v2 are_collinear or not v100,v101,v101 are_collinear or v2,v100,v101 are_collinear ) ;
hence ( v101 = v100 or not v100,v101,v2 are_collinear or v2,v100,v101 are_collinear ) by COLLSP:2; :: thesis: verum

end;

A50: ( not c7,c6,c5 are_collinear or c6,c5,c7 are_collinear ) by HESSENBE:1;

now :: thesis: ( ( c4,c7,c8 are_collinear or c9 = c7 or c10 = c5 or c10 = c3 or c10 = c2 or c1,c10,c5 are_collinear or c9 = c4 or c8 = c4 or c10 = c6 or c9,c4,c7 are_collinear ) & ( c7 = c4 or not c4,c7,c8 are_collinear or c8,c4,c7 are_collinear ) & ( not c1,c10,c5 are_collinear or c10,c5,c1 are_collinear ) & not c2,c6,c5 are_collinear & ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )

now :: thesis: ( ( c4,c10,c3 are_collinear or c4,c10,c2 are_collinear or c4,c10,c8 are_collinear or c4,c7,c8 are_collinear or c4,c10,c5 are_collinear or c4,c7,c9 are_collinear or c4,c10,c6 are_collinear or c4,c10,c9 are_collinear or c7,c10,c3 are_collinear or c7,c4,c9 are_collinear or c7,c10,c2 are_collinear or c7,c4,c8 are_collinear or c7,c6,c10 are_collinear or c9 = c7 or c10,c5,c7 are_collinear ) & ( not c10,c8,c4 are_collinear or c8,c4,c10 are_collinear ) & ( not c4,c10,c6 are_collinear or c10,c6,c4 are_collinear ) & ( not c4,c10,c5 are_collinear or c10,c5,c4 are_collinear ) & ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )

( c9,c7,c3 are_collinear & ( not c10,c9,c7 are_collinear or c9,c7,c10 are_collinear ) ) by A19, HESSENBE:1;
hence ( c4,c10,c3 are_collinear or c4,c10,c2 are_collinear or c4,c10,c8 are_collinear or c4,c7,c8 are_collinear or c4,c10,c5 are_collinear or c4,c7,c9 are_collinear or c4,c10,c6 are_collinear or c4,c10,c9 are_collinear or c7,c10,c3 are_collinear or c7,c4,c9 are_collinear or c7,c10,c2 are_collinear or c7,c4,c8 are_collinear or c7,c6,c10 are_collinear or c9 = c7 or c10,c5,c7 are_collinear ) by A30, A39, A36, A34, A32, A22, HESSENBE:1; :: thesis: ( ( not c10,c8,c4 are_collinear or c8,c4,c10 are_collinear ) & ( not c4,c10,c6 are_collinear or c10,c6,c4 are_collinear ) & ( not c4,c10,c5 are_collinear or c10,c5,c4 are_collinear ) & ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
thus ( not c10,c8,c4 are_collinear or c8,c4,c10 are_collinear ) by HESSENBE:1; :: thesis: ( ( not c4,c10,c6 are_collinear or c10,c6,c4 are_collinear ) & ( not c4,c10,c5 are_collinear or c10,c5,c4 are_collinear ) & ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
thus ( not c4,c10,c6 are_collinear or c10,c6,c4 are_collinear ) by HESSENBE:1; :: thesis: ( ( not c4,c10,c5 are_collinear or c10,c5,c4 are_collinear ) & ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
thus ( not c4,c10,c5 are_collinear or c10,c5,c4 are_collinear ) by HESSENBE:1; :: thesis: ( ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) & ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
thus ( not c7,c10,c3 are_collinear or c10,c3,c7 are_collinear ) by HESSENBE:1; :: thesis: ( ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) & ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
thus ( not c7,c10,c2 are_collinear or c10,c2,c7 are_collinear ) by HESSENBE:1; :: thesis: ( ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) & not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
thus ( not c10,c9,c4 are_collinear or c9,c4,c10 are_collinear ) by HESSENBE:1; :: thesis: ( not c6,c4,c2 are_collinear & c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )

now :: thesis: ( c6,c4,c6 are_collinear & not c4 = c6 & ( for v102, v104, v103, v101 being Element of PCPP holds
( v103 = v101 or not v101,v103,v102 are_collinear or not v101,v103,v104 are_collinear or v102,v103,v104 are_collinear ) ) )

thus c6,c4,c6 are_collinear by COLLSP:2; :: thesis: ( not c4 = c6 & ( for v102, v104, v103, v101 being Element of PCPP holds
( v103 = v101 or not v101,v103,v102 are_collinear or not v101,v103,v104 are_collinear or v102,v103,v104 are_collinear ) ) )
thus not c4 = c6 by COLLSP:2, A39; :: thesis: for v102, v104, v103, v101 being Element of PCPP holds
( v103 = v101 or not v101,v103,v102 are_collinear or not v101,v103,v104 are_collinear or v102,v103,v104 are_collinear )
thus for v102, v104, v103, v101 being Element of PCPP holds
( v103 = v101 or not v101,v103,v102 are_collinear or not v101,v103,v104 are_collinear or v102,v103,v104 are_collinear ) :: thesis: verum

proof

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

end;

end;

hence not c6,c4,c2 are_collinear by A48; :: thesis: ( c7,c6,c5 are_collinear & not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
c1,c7,c7 are_collinear by COLLSP:2;
hence c7,c6,c5 are_collinear by A23, A14, COLLSP:3, A15; :: thesis: ( not c5,c4,c3 are_collinear & not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )

now :: thesis: ( c5,c4,c4 are_collinear & ( not c4,c3,c5 are_collinear or c1,c5,c4 are_collinear ) )

thus c5,c4,c4 are_collinear by COLLSP:2; :: thesis: ( not c4,c3,c5 are_collinear or c1,c5,c4 are_collinear )
c4,c3,c4 are_collinear by COLLSP:2;
hence ( not c4,c3,c5 are_collinear or c1,c5,c4 are_collinear ) by A24, A5, COLLSP:3; :: thesis: verum

end;

hence not c5,c4,c3 are_collinear by A29, A38, COLLSP:3, A6, A26, A11; :: thesis: ( not c3,c7,c5 are_collinear & not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
c7,c5,c7 are_collinear by COLLSP:2;
then not c7,c5,c3 are_collinear by A35, A9, A25, COLLSP:3;
hence not c3,c7,c5 are_collinear by HESSENBE:1; :: thesis: ( not c2,c7,c6 are_collinear & c10,c6,c2 are_collinear )
thus not c2,c7,c6 are_collinear by HESSENBE:1, A40; :: thesis: c10,c6,c2 are_collinear
thus c10,c6,c2 are_collinear by A20, HESSENBE:1; :: thesis: verum

end;

then ( c4,c10,c2 are_collinear or c4,c7,c8 are_collinear or c4,c7,c9 are_collinear or c9 = c7 or c10 = c5 or c10 = c3 or c10 = c2 or c1,c10,c5 are_collinear or c9 = c4 or c8 = c4 or c10 = c6 or c10,c3,c4 are_collinear ) by A30, A45, A41, A43, A44, A47, A10, A27, COLLSP:3, A42, HESSENBE:1;
then A51: ( c4,c7,c8 are_collinear or c4,c7,c9 are_collinear or c9 = c7 or c10 = c5 or c10 = c3 or c10 = c2 or c1,c10,c5 are_collinear or c9 = c4 or c8 = c4 or c10 = c6 or c10,c2,c4 are_collinear ) by A46, A38, COLLSP:3, A6, A26, A11, A30, A44, HESSENBE:1;
not c7 = c4 by COLLSP:2, A11;
hence ( c4,c7,c8 are_collinear or c9 = c7 or c10 = c5 or c10 = c3 or c10 = c2 or c1,c10,c5 are_collinear or c9 = c4 or c8 = c4 or c10 = c6 or c9,c4,c7 are_collinear ) by A51, A49, A48, A43, A30; :: thesis: ( ( c7 = c4 or not c4,c7,c8 are_collinear or c8,c4,c7 are_collinear ) & ( not c1,c10,c5 are_collinear or c10,c5,c1 are_collinear ) & not c2,c6,c5 are_collinear & ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )
thus ( c7 = c4 or not c4,c7,c8 are_collinear or c8,c4,c7 are_collinear ) by A49; :: thesis: ( ( not c1,c10,c5 are_collinear or c10,c5,c1 are_collinear ) & not c2,c6,c5 are_collinear & ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )
thus ( not c1,c10,c5 are_collinear or c10,c5,c1 are_collinear ) by HESSENBE:1; :: thesis: ( not c2,c6,c5 are_collinear & ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )
A52: not c4 = c1 by COLLSP:2, A11;
( ( not c6,c5,c2 are_collinear or c5,c2,c7 are_collinear ) & c2,c6,c2 are_collinear & not c4 = c1 & not c6 = c2 & c5,c2,c2 are_collinear & c5,c2,c5 are_collinear & not c2 = c5 ) by A40, A11, A50, A30, A8, A23, A14, A15, COLLSP:2;
hence not c2,c6,c5 are_collinear by A30, COLLSP:3, A37; :: thesis: ( ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) & ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )

now :: thesis: ( c3,c2,c1 are_collinear & not c1,c6,c3 are_collinear )

c1,c4,c1 are_collinear by COLLSP:2;
hence c3,c2,c1 are_collinear by A52, A12, COLLSP:3, A13; :: thesis: not c1,c6,c3 are_collinear
c1,c6,c1 are_collinear by COLLSP:2;
hence not c1,c6,c3 are_collinear by A35, A7, A28, COLLSP:3; :: thesis: verum

end;

hence ( ( not c3,c2,c6 are_collinear & not c3,c2,c5 are_collinear ) or c1,c5,c3 are_collinear ) by A29, A3; :: thesis: ( ( for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) ) & not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )
thus for v102, v103, v104, v101 being Element of PCPP holds
( v104 = v101 or not v101,v104,v102 are_collinear or not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear ) :: thesis: ( not c5,c1,c3 are_collinear & c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )

proof

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

end;

( c5,c1,c1 are_collinear & c5,c1,c7 are_collinear ) by COLLSP:2, A14, HESSENBE:1;
hence not c5,c1,c3 are_collinear by A35, A6, COLLSP:3; :: thesis: ( c8,c2,c7 are_collinear & not c3,c7,c4 are_collinear )
thus c8,c2,c7 are_collinear by A17, HESSENBE:1; :: thesis: not c3,c7,c4 are_collinear
( c3,c7,c7 are_collinear & c3,c7,c3 are_collinear & not c7 = c3 ) by COLLSP:2, A34;
hence not c3,c7,c4 are_collinear by COLLSP:3, A34; :: thesis: verum

end;

hence contradiction by A30, A45, HESSENBE:1, A36, A42, COLLSP:2, A41, A23, A14, A15, A50, A47, A32, A39, A19, A20; :: thesis: verum