let PCPP be CollProjectiveSpace; :: thesis: for c1, c2, c3, c4, c5, c6, c7, c8, c10 being Element of PCPP st not c2 = c1 & not c3 = c2 & not c5 = c1 & not c7 = c5 & not 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 & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear holds
not c10,c7,c8 are_collinear
let c1, c2, c3, c4, c5, c6, c7, c8, c10 be Element of PCPP; :: thesis: ( not c2 = c1 & not c3 = c2 & not c5 = c1 & not c7 = c5 & not 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 & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear implies not c10,c7,c8 are_collinear )
assume that
A1: not c2 = c1 and
A2: not c3 = c2 and
A3: not c5 = c1 and
A4: not c7 = c5 and
A5: not c7 = c6 and
A6: not c1,c4,c7 are_collinear and
A7: c1,c4,c2 are_collinear and
A8: c1,c4,c3 are_collinear and
A9: c1,c7,c5 are_collinear and
A10: c1,c7,c6 are_collinear and
A11: c4,c5,c8 are_collinear and
A12: c7,c2,c8 are_collinear and
A13: c2,c6,c10 are_collinear and
A14: c3,c5,c10 are_collinear and
A15: c10,c7,c8 are_collinear ; :: thesis: contradiction
A16: not c4 = c1 by COLLSP:2, A6;
now :: thesis: ( not c3,c2,c5 are_collinear & ( c8 = c7 or not c7,c8,c2 are_collinear or c10,c2,c7 are_collinear ) & ( c10 = c2 or not c2,c10,c7 are_collinear or c6,c7,c2 are_collinear ) & not c7,c6,c2 are_collinear & not c7,c5,c4 are_collinear )
now :: thesis: ( c3,c2,c4 are_collinear & ( not c1,c3,c2 are_collinear or c3,c2,c1 are_collinear ) & not c1,c5,c4 are_collinear & c1,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 ) ) & c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )
c1,c4,c4 are_collinear by COLLSP:2;
hence c3,c2,c4 are_collinear by A8, A7, A16, COLLSP:3; :: thesis: ( ( not c1,c3,c2 are_collinear or c3,c2,c1 are_collinear ) & not c1,c5,c4 are_collinear & c1,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 ) ) & c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )
thus ( not c1,c3,c2 are_collinear or c3,c2,c1 are_collinear ) by HESSENBE:1; :: thesis: ( not c1,c5,c4 are_collinear & c1,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 ) ) & c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )
( c1,c5,c1 are_collinear & c1,c5,c7 are_collinear ) by COLLSP:2, A9, HESSENBE:1;
hence not c1,c5,c4 are_collinear by A3, COLLSP:3, A6; :: thesis: ( c1,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 ) ) & c7,c8,c10 are_collinear & c2,c10,c6 are_collinear )
thus c1,c4,c1 are_collinear by COLLSP:2; :: 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 ) ) & c7,c8,c10 are_collinear & c2,c10,c6 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: ( c7,c8,c10 are_collinear & c2,c10,c6 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 c7,c8,c10 are_collinear by A15, HESSENBE:1; :: thesis: c2,c10,c6 are_collinear
thus c2,c10,c6 are_collinear by A13, HESSENBE:1; :: thesis: verum
end;
hence ( not c3,c2,c5 are_collinear & ( c8 = c7 or not c7,c8,c2 are_collinear or c10,c2,c7 are_collinear ) & ( c10 = c2 or not c2,c10,c7 are_collinear or c6,c7,c2 are_collinear ) ) by A7, A16, A8, A2, COLLSP:3; :: thesis: ( not c7,c6,c2 are_collinear & not c7,c5,c4 are_collinear )
now :: thesis: ( c7,c6,c7 are_collinear & not c1,c2,c7 are_collinear & c7,c6,c1 are_collinear )
thus c7,c6,c7 are_collinear by COLLSP:2; :: thesis: ( not c1,c2,c7 are_collinear & c7,c6,c1 are_collinear )
( c1,c2,c1 are_collinear & c1,c2,c4 are_collinear ) by COLLSP:2, A7, HESSENBE:1;
hence not c1,c2,c7 are_collinear by A1, COLLSP:3, A6; :: thesis: c7,c6,c1 are_collinear
thus c7,c6,c1 are_collinear by A10, HESSENBE:1; :: thesis: verum
end;
hence not c7,c6,c2 are_collinear by A5, COLLSP:3; :: thesis: not c7,c5,c4 are_collinear
( c7,c5,c7 are_collinear & c7,c5,c1 are_collinear ) by COLLSP:2, A9, HESSENBE:1;
hence not c7,c5,c4 are_collinear by COLLSP:3, A4, A6; :: thesis: verum
end;
hence contradiction by A11, HESSENBE:1, A12, A14; :: thesis: verum