let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, b9, c9 being Element of FCPS st not a,b,c is_collinear & a,b,b9 is_collinear & a,c,c9 is_collinear & a <> b9 holds
b9 <> c9
let a, b, c, b9, c9 be Element of FCPS; :: thesis: ( not a,b,c is_collinear & a,b,b9 is_collinear & a,c,c9 is_collinear & a <> b9 implies b9 <> c9 )
assume that
A1: not a,b,c is_collinear and
A2: a,b,b9 is_collinear and
A3: a,c,c9 is_collinear and
A4: a <> b9 ; :: thesis: b9 <> c9
assume not b9 <> c9 ; :: thesis: contradiction
then A5: a,b9,c is_collinear by A3, Th1;
a,b9,b is_collinear by A2, Th1;
hence contradiction by A1, A4, A5, COLLSP:11; :: thesis: verum