let P, Q be Element of real_projective_plane; :: thesis: ( P in absolute & Q in BK_model implies ex R being Element of real_projective_plane st
( R in BK_model & Q <> R & R,Q,P are_collinear ) )
assume that
A1: P in absolute and
A2: Q in BK_model ; :: thesis: ex R being Element of real_projective_plane st
( R in BK_model & Q <> R & R,Q,P are_collinear )
reconsider QBK = Q as Element of BK_model by A2;
consider u being non zero Element of (TOP-REAL 3) such that
((u . 1) ^2) + ((u . 2) ^2) = 1 and
A3: u . 3 = 1 and
A4: P = Dir u by A1, BKMODEL1:89;
consider v being non zero Element of (TOP-REAL 3) such that
A5: ( Dir v = QBK & v . 3 = 1 & BK_to_REAL2 QBK = |[(v . 1),(v . 2)]| ) by Def01;
not |[(((v . 1) + (u . 1)) / 2),(((v . 2) + (u . 2)) / 2),1]| is zero by EUCLID_5:4, FINSEQ_1:78;
then reconsider w = |[(((v . 1) + (u . 1)) / 2),(((v . 2) + (u . 2)) / 2),1]| as non zero Element of (TOP-REAL 3) ;
reconsider R = Dir w as Element of real_projective_plane by ANPROJ_1:26;
take R ; :: thesis: ( R in BK_model & Q <> R & R,Q,P are_collinear )

now :: thesis: ( u = |[(u . 1),(u . 2),1]| & v = |[(v . 1),(v . 2),1]| )

( u = |[(u `1),(u `2),(u `3)]| & v = |[(v `1),(v `2),(v `3)]| ) by EUCLID_5:3;
then ( u = |[(u . 1),(u `2),(u `3)]| & v = |[(v . 1),(v `2),(v `3)]| ) ;
then ( u = |[(u . 1),(u . 2),(u `3)]| & v = |[(v . 1),(v . 2),(v `3)]| ) ;
hence ( u = |[(u . 1),(u . 2),1]| & v = |[(v . 1),(v . 2),1]| ) by A3, A5; :: thesis: verum

end;

then ( R in BK_model & R <> Q & Q,R,P are_collinear ) by A1, A4, A5, Th13;
hence ( R in BK_model & Q <> R & R,Q,P are_collinear ) by COLLSP:4; :: thesis: verum