let PCPP be CollProjectiveSpace; :: thesis: for c1, c2, c5, c6, c7 being Element of PCPP st not c1,c2,c5 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear holds
c5,c6,c7 are_collinear
let c1, c2, c5, c6, c7 be Element of PCPP; :: thesis: ( not c1,c2,c5 are_collinear & c1,c5,c6 are_collinear & c1,c5,c7 are_collinear implies c5,c6,c7 are_collinear )
assume that
A1: not c1,c2,c5 are_collinear and
A2: c1,c5,c6 are_collinear and
A3: c1,c5,c7 are_collinear and
A4: not c5,c6,c7 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,c5,v0 are_collinear or v0,c6,c7 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,c5,v0 are_collinear or v0,c6,c7 are_collinear )
( not c5 = c1 or c1,c2,c5 are_collinear ) by COLLSP:2;
hence for v0 being Element of PCPP holds
( not c1,c5,v0 are_collinear or v0,c6,c7 are_collinear ) by COLLSP:3, A1, A2, A3; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum