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