let P, Q be Element of BK_model ; :: thesis: for P1, P2, P3 being Element of absolute st P <> Q & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,Q,P3 are_collinear & not P3 = P1 holds
P3 = P2
let P1, P2, P3 be Element of absolute ; :: thesis: ( P <> Q & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,Q,P3 are_collinear & not P3 = P1 implies P3 = P2 )
assume that
A1: P <> Q and
A2: P1 <> P2 and
A3: P,Q,P1 are_collinear and
A4: P,Q,P2 are_collinear and
A5: P,Q,P3 are_collinear ; :: thesis: ( P3 = P1 or P3 = P2 )
( P3 = P1 or P3 = P2 )

proof

assume ( P3 <> P1 & P3 <> P2 ) ; :: thesis: contradiction
then P1,P2,P3 are_mutually_distinct by A2;
hence contradiction by A1, A3, A4, A5, COLLSP:3, BKMODEL1:92; :: thesis: verum

end;

hence ( P3 = P1 or P3 = P2 ) ; :: thesis: verum