let PCPP be CollProjectiveSpace; :: thesis: for c1, c2, c3, c4, c5 being Element of PCPP st not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c2,c4 are_collinear holds
c2,c3,c4 are_collinear
let c1, c2, c3, c4, c5 be Element of PCPP; :: thesis: ( not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c2,c4 are_collinear implies c2,c3,c4 are_collinear )
assume that
A1: not c1,c2,c5 are_collinear and
A2: c1,c2,c3 are_collinear and
A3: c1,c2,c4 are_collinear and
A4: not c2,c3,c4 are_collinear ; :: thesis: contradiction

now :: thesis: ( ( for v100, v2 being Element of PCPP holds v2,v100,v100 are_collinear ) & ( for v0 being Element of PCPP holds
( not c1,c2,v0 are_collinear or not c1,c2,c4 are_collinear or v0,c3,c4 are_collinear ) ) )

thus for v100, v2 being Element of PCPP holds v2,v100,v100 are_collinear by COLLSP:2; :: thesis: for v0 being Element of PCPP holds
( not c1,c2,v0 are_collinear or not c1,c2,c4 are_collinear or v0,c3,c4 are_collinear )
( not c2 = c1 or c1,c2,c5 are_collinear ) by COLLSP:2;
hence for v0 being Element of PCPP holds
( not c1,c2,v0 are_collinear or not c1,c2,c4 are_collinear or v0,c3,c4 are_collinear ) by A2, COLLSP:3, A1; :: thesis: verum

end;

hence contradiction by A3, A4; :: thesis: verum