let P, Q be Element of real_projective_plane; ( 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
; 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
; ( R in BK_model & Q <> R & R,Q,P are_collinear )
now ( 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)]| )
by EUCLID_5:def 1;
then
(
u = |[(u . 1),(u . 2),(u `3)]| &
v = |[(v . 1),(v . 2),(v `3)]| )
by EUCLID_5:def 2;
hence
(
u = |[(u . 1),(u . 2),1]| &
v = |[(v . 1),(v . 2),1]| )
by EUCLID_5:def 3, A3, A5;
verum
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; verum