let P, Q, R be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u, v, w being non zero Element of (TOP-REAL 3) st P in absolute & Q in absolute & P <> Q & P = Dir u & Q = Dir v & R = Dir w & u `3 = 1 & v `3 = 1 & w = |[(((u `1) + (v `1)) / 2),(((u `2) + (v `2)) / 2),1]| holds
R in BK_model
let u, v, w be non zero Element of (TOP-REAL 3); :: thesis: ( P in absolute & Q in absolute & P <> Q & P = Dir u & Q = Dir v & R = Dir w & u `3 = 1 & v `3 = 1 & w = |[(((u `1) + (v `1)) / 2),(((u `2) + (v `2)) / 2),1]| implies R in BK_model )
assume that
A1: P in absolute and
A2: Q in absolute and
A3: P <> Q and
A4: ( P = Dir u & Q = Dir v & R = Dir w ) and
A5: ( u `3 = 1 & v `3 = 1 ) and
A6: w = |[(((u `1) + (v `1)) / 2),(((u `2) + (v `2)) / 2),1]| ; :: thesis: R in BK_model
A7: ( u . 3 = 1 & v . 3 = 1 ) by A5, EUCLID_5:def 3;
reconsider u9 = |[(u . 1),(u . 2)]|, v9 = |[(v . 1),(v . 2)]| as Element of (TOP-REAL 2) ;
set M = the_midpoint_of_the_segment (u9,v9);
A8: ( w `1 = (((u `1) + (v `1)) * 1) / 2 & w `2 = (((u `2) + (v `2)) * 1) / 2 ) by A6, EUCLID_5:2;
A9: the_midpoint_of_the_segment (u9,v9) = (1 / 2) * (u9 + v9) by EUCLID12:29
.= (1 / 2) * |[((u . 1) + (v . 1)),((u . 2) + (v . 2))]| by EUCLID:56
.= |[((((u . 1) + (v . 1)) * 1) / 2),((((u . 2) + (v . 2)) * 1) / 2)]| by EUCLID:58
.= |[((((u `1) + (v . 1)) * 1) / 2),((((u . 2) + (v . 2)) * 1) / 2)]| by EUCLID_5:def 1
.= |[((((u `1) + (v . 1)) * 1) / 2),((((u `2) + (v . 2)) * 1) / 2)]| by EUCLID_5:def 2
.= |[((((u `1) + (v `1)) * 1) / 2),((((u `2) + (v . 2)) * 1) / 2)]| by EUCLID_5:def 1
.= |[(w `1),(w `2)]| by A8, EUCLID_5:def 2 ;
( u9 in circle (0,0,1) & v9 in circle (0,0,1) ) by A7, A1, A2, A4, BKMODEL1:84;
then A10: (LSeg (u9,v9)) \ {u9,v9} c= inside_of_circle (0,0,1) by TOPREAL9:60;
u9 <> v9

proof

assume u9 = v9 ; :: thesis: contradiction
then ( u . 1 = v . 1 & u . 2 = v . 2 ) by FINSEQ_1:77;
then ( u `1 = v . 1 & u `2 = v . 2 ) by EUCLID_5:def 1, EUCLID_5:def 2;
then ( u `1 = v `1 & u `2 = v `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;
then u = |[(v `1),(v `2),(v `3)]| by A5, EUCLID_5:3
.= v by EUCLID_5:3 ;
hence contradiction by A4, A3; :: thesis: verum

end;

then ( the_midpoint_of_the_segment (u9,v9) <> u9 & the_midpoint_of_the_segment (u9,v9) <> v9 ) by EUCLID12:32, EUCLID12:33;
then A11: not the_midpoint_of_the_segment (u9,v9) in {u9,v9} by TARSKI:def 2;
the_midpoint_of_the_segment (u9,v9) in LSeg (u9,v9) by EUCLID12:28;
then the_midpoint_of_the_segment (u9,v9) in (LSeg (u9,v9)) \ {u9,v9} by A11, XBOOLE_0:def 5;
then reconsider rw = |[(w `1),(w `2)]| as Element of inside_of_circle (0,0,1) by A10, A9;
consider RW2 being Element of (TOP-REAL 2) such that
A12: ( RW2 = rw & REAL2_to_BK rw = Dir |[(RW2 `1),(RW2 `2),1]| ) by BKMODEL2:def 3;
A13: ( rw `1 = w `1 & rw `2 = w `2 ) by EUCLID:52;
|[(RW2 `1),(RW2 `2),1]| = |[(w `1),(w `2),(w `3)]| by A12, A13, A6, EUCLID_5:2
.= w by EUCLID_5:3 ;
hence R in BK_model by A12, A4; :: thesis: verum