let c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis:
assume that
A1: c1 <> c2 and
A2: c3 <> c1 and
A3: c2 <> c3 and
A4: c2 <> c4 and
A5: c3 <> c4 and
A6: c1 <> c5 and
A7: c1 <> c6 and
A8: c5 <> c6 and
A9: c5 <> c7 and
A10: c6 <> c7 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 ; :: thesis:
assume A22: ( c4,c2,c7 are_collinear or c4,c3,c7 are_collinear or c2,c3,c7 are_collinear or c4,c2,c5 are_collinear or c4,c2,c6 are_collinear or c4,c3,c5 are_collinear or c4,c3,c6 are_collinear or c2,c7,c5 are_collinear or c2,c7,c6 are_collinear or c3,c7,c5 are_collinear or c3,c7,c6 are_collinear or c2,c3,c5 are_collinear or c2,c3,c6 are_collinear or c7,c5,c4 are_collinear or c7,c6,c4 are_collinear or c5,c6,c4 are_collinear or c5,c6,c2 are_collinear or not c4,c5,c8 are_collinear or not c4,c6,c9 are_collinear or not c2,c7,c8 are_collinear or not c2,c6,c10 are_collinear or not c3,c7,c9 are_collinear or not c3,c5,c10 are_collinear ) ; :: thesis:

thus not c1,c7,c4 are_collinear by COLLSP:4, A11; :: thesis:
thus c4,c2,c1 are_collinear by A12, HESSENBE:1; :: thesis:
thus c4,c3,c1 are_collinear by HESSENBE:1, A13; :: thesis:
thus not c2,c3,c7 are_collinear by A3, A11, A12, A13, HESSENBE:3; :: thesis:
thus c1,c5,c7 are_collinear by A14, COLLSP:4; :: thesis:
thus c7,c1,c5 are_collinear by A14, COLLSP:4; :: thesis:
thus c7,c6,c1 are_collinear by HESSENBE:1, A15; :: thesis:
thus c1,c6,c7 are_collinear by A15, COLLSP:4; :: thesis:
thus c7,c1,c6 are_collinear by A15, COLLSP:4; :: thesis:
( ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c4,c4 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c4,c4 are_collinear or not v100,c4,c3 are_collinear or not c4,c3,v2 are_collinear or v100,c4,v2 are_collinear ) ) ) by COLLSP:2, A5, HESSENBE:3;
hence not c4,c3,c7 are_collinear by A11, A13; :: thesis:
( ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c4,c4 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c4,c4 are_collinear or not v100,c4,c2 are_collinear or not c4,c2,v2 are_collinear or v100,c4,v2 are_collinear ) ) ) by COLLSP:2, A4, HESSENBE:3;
hence not c4,c2,c7 are_collinear by A11, A12; :: thesis:
( ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c1,c1 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c1,c1 are_collinear or not v100,c1,c2 are_collinear or not c1,c2,v2 are_collinear or v100,c1,v2 are_collinear ) ) & c1,c2,c4 are_collinear & not c7,c1,c4 are_collinear ) by A12, COLLSP:2, A1, HESSENBE:1, HESSENBE:3, A11;
hence not c7,c1,c2 are_collinear ; :: thesis:
thus for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) by A10, HESSENBE:3; :: thesis:
thus for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear by COLLSP:2; :: thesis:
thus for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) by A9, HESSENBE:3; :: thesis:

thus c3,c7,c7 are_collinear by COLLSP:2; :: thesis:
c1,c4,c1 are_collinear by COLLSP:2;
hence not c3,c1,c7 are_collinear by A11, A2, A13, HESSENBE:3; :: thesis:

end;

hence not c3,c7,c1 are_collinear by HESSENBE:2, A11, A13; :: thesis:
thus c5,c7,c1 are_collinear by HESSENBE:1, A14; :: thesis:

thus c2,c7,c7 are_collinear by COLLSP:2; :: thesis:
c1,c4,c1 are_collinear by COLLSP:2;
hence not c2,c1,c7 are_collinear by A11, A1, A12, HESSENBE:3; :: thesis:

end;

hence not c2,c7,c1 are_collinear by A11, A12, HESSENBE:2; :: thesis:
not c4 = c1 by COLLSP:2, A11;
then c1,c2,c3 are_collinear by A13, A12, HESSENBE:2;
hence c2,c3,c1 are_collinear by HESSENBE:1; :: thesis:

hereby :: thesis:

let v2, v100 be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis:
( not v100,c7,c5 are_collinear or not v100,c7,c7 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) by A9, HESSENBE:3;
hence ( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) by COLLSP:2; :: thesis:

end;

end;

hence contradiction by A6, HESSENBE:3, A17, A16, A18, A19, A20, A21, A22, COLLSP:4, A15, A8, A14, A7; :: thesis: