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