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