let P, Q, R be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); 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); ( 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]|
; 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
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; verum