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