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