let R1, R2 be Point of TarskiEuclid2Space; :: thesis: ( 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 ) ; :: thesis: 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 :: thesis: ( 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 :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: ( |[(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; :: thesis: |[(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; :: thesis: verum

end;

then P9 is Element of absolute by BKMODEL1:86;
hence P9 in absolute ; :: thesis: ( Q9 in absolute & P9 <> Q9 & u9 `3 = 1 & v9 `3 = 1 & w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]| )

now :: thesis: ( Q9 = Dir v9 & v9 . 3 = 1 & |[(v9 . 1),(v9 . 2)]| in circle (0,0,1) )

thus Q9 = Dir v9 ; :: thesis: ( 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; :: thesis: |[(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; :: thesis: verum

end;

then Q9 is Element of absolute by BKMODEL1:86;
hence Q9 in absolute ; :: thesis: ( P9 <> Q9 & u9 `3 = 1 & v9 `3 = 1 & w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]| )
thus P9 <> Q9 :: thesis: ( u9 `3 = 1 & v9 `3 = 1 & w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]| )

proof

assume A8: P9 = Q9 ; :: thesis: contradiction

now :: thesis: ( Dir u9 = Dir v9 & u9 . 3 = 1 & v9 . 3 = 1 )

thus Dir u9 = Dir v9 by A8; :: thesis: ( u9 . 3 = 1 & v9 . 3 = 1 )
thus u9 . 3 = u9 `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: v9 . 3 = 1
thus v9 . 3 = v9 `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: verum

end;

then u9 = v9 by BKMODEL1:43;
then ( P `1 = Q `1 & P `2 = Q `2 ) by FINSEQ_1:78;
then |[(P `1),(P `2)]| = Q by EUCLID:53;
hence contradiction by A1, EUCLID:53; :: thesis: verum

end;

thus ( u9 `3 = 1 & v9 `3 = 1 ) by EUCLID_5:2; :: thesis: 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]| :: thesis: verum

proof

( u9 `1 = P `1 & v9 `1 = Q `1 & u9 `2 = P `2 & v9 `2 = Q `2 & w `1 = ((P `1) + (Q `1)) / 2 & w `2 = ((P `2) + (Q `2)) / 2 ) by EUCLID:52, EUCLID_5:2;
hence w9 = |[(((u9 `1) + (v9 `1)) / 2),(((u9 `2) + (v9 `2)) / 2),1]| ; :: thesis: verum

end;

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 ; :: thesis: between R1, BK_to_T2 AR9,R2

now :: thesis: ( R99 = RP3_to_T2 R9 & RP3_to_T2 R9 = BK_to_T2 AR9 )

thus R99 = RP3_to_T2 R9 ; :: thesis: RP3_to_T2 R9 = BK_to_T2 AR9
consider x being non zero Element of (TOP-REAL 3) such that
A11: ( Dir x = r & x . 3 = 1 & BK_to_REAL2 r = |[(x . 1),(x . 2)]| ) by BKMODEL2:def 2;

now :: thesis: ( Dir x = Dir w9 & x . 3 <> 0 & x . 3 = w9 . 3 )

thus Dir x = Dir w9 by A11, A9; :: thesis: ( x . 3 <> 0 & x . 3 = w9 . 3 )
thus x . 3 <> 0 by A11; :: thesis: x . 3 = w9 . 3
w9 . 3 = w9 `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ;
hence x . 3 = w9 . 3 by A11; :: thesis: verum

end;

then x = w9 by Th16;
then BK_to_REAL2 r = |[(w9 `1),(w9 . 2)]| by A11, EUCLID_5:def 1
.= |[(w `1),(w `2)]| by A4, EUCLID_5:def 2
.= w by EUCLID:53 ;
hence RP3_to_T2 R9 = BK_to_T2 AR9 by A3, A5, A4, EUCLID:53, A10; :: thesis: verum

end;

hence between R1, BK_to_T2 AR9,R2 by A7, A6, GTARSKI2:20; :: thesis: verum