let P be Element of BK_model ; :: thesis: ex P1, P2 being Element of absolute st
( P1 <> P2 & P1,P,P2 are_collinear )
consider Q being Element of BK_model such that
A1: P <> Q by Th11;
consider P1, P2 being Element of absolute such that
A2: P1 <> P2 and
A3: P,Q,P1 are_collinear and
A4: P,Q,P2 are_collinear by A1, BKMODEL2:20;
take P1 ; :: thesis: ex P2 being Element of absolute st
( P1 <> P2 & P1,P,P2 are_collinear )
take P2 ; :: thesis: ( P1 <> P2 & P1,P,P2 are_collinear )
P,P1,P2 are_collinear by A1, A3, A4, COLLSP:6;
hence ( P1 <> P2 & P1,P,P2 are_collinear ) by A2, COLLSP:4; :: thesis: verum