let PCPP be CollProjectiveSpace; :: thesis: for c1, c2, c3, c5, c7 being Element of PCPP st c3 <> c1 & not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c5,c7 are_collinear holds
c7 <> c3
let c1, c2, c3, c5, c7 be Element of PCPP; :: thesis: ( c3 <> c1 & not c1,c2,c5 are_collinear & c1,c2,c3 are_collinear & c1,c5,c7 are_collinear implies c7 <> c3 )
assume that
A1: not c3 = c1 and
A2: not c1,c2,c5 are_collinear and
A3: c1,c2,c3 are_collinear and
A4: c1,c5,c7 are_collinear and
A5: c7 = c3 ; :: thesis: contradiction
( c3,c1,c2 are_collinear & c3,c1,c5 are_collinear & c3,c1,c1 are_collinear ) by A3, A4, A5, HESSENBE:1, COLLSP:2;
hence contradiction by A1, COLLSP:3, A2; :: thesis: verum