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