let P be Element of BK_model ; :: thesis: for Q being Element of absolute ex R being Element of BK_model st

( P <> R & P,Q,R are_collinear )

let Q be Element of absolute ; :: thesis: ex R being Element of BK_model st

( P <> R & P,Q,R are_collinear )

reconsider P1 = P, Q1 = Q as Element of real_projective_plane ;

consider R1 being Element of real_projective_plane such that

A1: R1 in BK_model and

A2: P1 <> R1 and

A3: R1,P1,Q1 are_collinear by BKMODEL2:22;

reconsider R = R1 as Element of BK_model by A1;

take R ; :: thesis: ( P <> R & P,Q,R are_collinear )

thus ( P <> R & P,Q,R are_collinear ) by A3, A2, HESSENBE:1; :: thesis: verum

( P <> R & P,Q,R are_collinear )

let Q be Element of absolute ; :: thesis: ex R being Element of BK_model st

( P <> R & P,Q,R are_collinear )

reconsider P1 = P, Q1 = Q as Element of real_projective_plane ;

consider R1 being Element of real_projective_plane such that

A1: R1 in BK_model and

A2: P1 <> R1 and

A3: R1,P1,Q1 are_collinear by BKMODEL2:22;

reconsider R = R1 as Element of BK_model by A1;

take R ; :: thesis: ( P <> R & P,Q,R are_collinear )

thus ( P <> R & P,Q,R are_collinear ) by A3, A2, HESSENBE:1; :: thesis: verum