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

( 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