let R1, R2 be Point of TarskiEuclid2Space; ( Tn2TR R1 in circle (0,0,1) & Tn2TR R2 in circle (0,0,1) & R1 <> R2 implies ex P being Element of BK-model-Plane st between R1, BK_to_T2 P,R2 )
assume A1:
( Tn2TR R1 in circle (0,0,1) & Tn2TR R2 in circle (0,0,1) & R1 <> R2 )
; ex P being Element of BK-model-Plane st between R1, BK_to_T2 P,R2
reconsider P = Tn2TR R1, Q = Tn2TR R2 as Element of (TOP-REAL 2) ;
A2:
( P = |[(P `1),(P `2)]| & Q = |[(Q `1),(Q `2)]| )
by EUCLID:53;
reconsider w = |[(((P `1) + (Q `1)) / 2),(((P `2) + (Q `2)) / 2)]| as Element of (TOP-REAL 2) ;
reconsider u9 = |[(P `1),(P `2),1]|, v9 = |[(Q `1),(Q `2),1]| as non zero Element of (TOP-REAL 3) ;
reconsider w9 = |[(w `1),(w `2),1]| as non zero Element of (TOP-REAL 3) ;
reconsider P9 = Dir u9, Q9 = Dir v9, R9 = Dir w9 as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
( u9 `3 = 1 & v9 `3 = 1 )
by EUCLID_5:2;
then reconsider P9 = P9, Q9 = Q9 as non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)) by Th40;
w9 `3 <> 0
by EUCLID_5:2;
then reconsider R9 = R9 as non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)) by Th40;
reconsider R99 = RP3_to_T2 R9 as Point of TarskiEuclid2Space ;
consider w99 being non zero Element of (TOP-REAL 3) such that
A3:
( R9 = Dir w99 & w99 `3 = 1 & RP3_to_REAL2 R9 = |[(w99 `1),(w99 `2)]| )
by Def05;
A4:
( w9 `1 = w `1 & w9 `2 = w `2 )
by EUCLID_5:2;
( w99 . 3 = 1 & w9 `3 = 1 )
by A3, EUCLID_5:2, EUCLID_5:def 3;
then
( w99 . 3 = w9 . 3 & w9 . 3 <> 0 )
by EUCLID_5:def 3;
then A5:
w99 = w9
by A3, BKMODEL1:43;
A6:
Tn2TR R99 = w
by A3, A5, A4, EUCLID:53;
w =
|[(((P `1) / 2) + ((Q `1) / 2)),(((P `2) / 2) + ((Q `2) / 2))]|
.=
|[((P `1) / 2),((P `2) / 2)]| + |[((Q `1) / 2),((Q `2) / 2)]|
by EUCLID:56
.=
((1 / 2) * |[(P `1),(P `2)]|) + |[((Q `1) / 2),((Q `2) / 2)]|
by EUCLID:58
.=
((1 - (1 / 2)) * P) + ((1 / 2) * Q)
by A2, EUCLID:58
;
then
w in { (((1 - r) * P) + (r * Q)) where r is Real : ( 0 <= r & r <= 1 ) }
;
then A7:
w in LSeg ((Tn2TR R1),(Tn2TR R2))
by RLTOPSP1:def 2;
now ( P9 in absolute & Q9 in absolute & P9 <> Q9 & u9 `3 = 1 & v9 `3 = 1 & w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]| )now ( P9 = Dir u9 & u9 . 3 = 1 & |[(P `1),(P `2)]| in circle (0,0,1) & |[(u9 . 1),(u9 . 2)]| in circle (0,0,1) )thus
P9 = Dir u9
;
( u9 . 3 = 1 & |[(P `1),(P `2)]| in circle (0,0,1) & |[(u9 . 1),(u9 . 2)]| in circle (0,0,1) )
u9 `3 = 1
by EUCLID_5:2;
hence
u9 . 3
= 1
by EUCLID_5:def 3;
( |[(P `1),(P `2)]| in circle (0,0,1) & |[(u9 . 1),(u9 . 2)]| in circle (0,0,1) )thus
|[(P `1),(P `2)]| in circle (
0,
0,1)
by A1, EUCLID:53;
|[(u9 . 1),(u9 . 2)]| in circle (0,0,1)
(
u9 `1 = P `1 &
u9 `2 = P `2 )
by EUCLID_5:2;
then
(
P `1 = u9 . 1 &
P `2 = u9 . 2 )
by EUCLID_5:def 1, EUCLID_5:def 2;
hence
|[(u9 . 1),(u9 . 2)]| in circle (
0,
0,1)
by A1, EUCLID:53;
verum end; then
P9 is
Element of
absolute
by BKMODEL1:86;
hence
P9 in absolute
;
( Q9 in absolute & P9 <> Q9 & u9 `3 = 1 & v9 `3 = 1 & w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]| )now ( Q9 = Dir v9 & v9 . 3 = 1 & |[(v9 . 1),(v9 . 2)]| in circle (0,0,1) )thus
Q9 = Dir v9
;
( v9 . 3 = 1 & |[(v9 . 1),(v9 . 2)]| in circle (0,0,1) )
v9 `3 = 1
by EUCLID_5:2;
hence
v9 . 3
= 1
by EUCLID_5:def 3;
|[(v9 . 1),(v9 . 2)]| in circle (0,0,1)
(
v9 `1 = Q `1 &
v9 `2 = Q `2 )
by EUCLID_5:2;
then
(
Q `1 = v9 . 1 &
Q `2 = v9 . 2 )
by EUCLID_5:def 1, EUCLID_5:def 2;
hence
|[(v9 . 1),(v9 . 2)]| in circle (
0,
0,1)
by A1, EUCLID:53;
verum end; then
Q9 is
Element of
absolute
by BKMODEL1:86;
hence
Q9 in absolute
;
( P9 <> Q9 & u9 `3 = 1 & v9 `3 = 1 & w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]| )thus
P9 <> Q9
( u9 `3 = 1 & v9 `3 = 1 & w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]| )thus
(
u9 `3 = 1 &
v9 `3 = 1 )
by EUCLID_5:2;
w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]|thus
w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]|
verum end;
then reconsider AR9 = R9 as Element of BK-model-Plane by Th48;
consider r being Element of BK_model such that
A9:
AR9 = r
and
A10:
BK_to_T2 AR9 = BK_to_REAL2 r
by Def01;
take
AR9
; between R1, BK_to_T2 AR9,R2
hence
between R1, BK_to_T2 AR9,R2
by A7, A6, GTARSKI2:20; verum