let X, Y be Subset of TarskiEuclid2Space; :: thesis:
given a being Element of TarskiEuclid2Space such that A1: for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y ; :: thesis:

per cases ;

suppose SS: ( X c= {a} or Y = {} ) ; :: thesis:

ex b being Element of TarskiEuclid2Space st
for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between x,b,y

proof

take b = a; :: thesis:
let x, y be Element of TarskiEuclid2Space; :: thesis:
assume ( x in X & y in Y ) ; :: thesis:
then x = a by SS, TARSKI:def 1;
hence between x,b,y by GTARSKI1:17; :: thesis:

end;

hence ex b being Element of TarskiEuclid2Space st
for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between x,b,y ; :: thesis:

end;

suppose SSS: ( not X c= {a} & Y <> {} ) ; :: thesis:

X \ {a} <> {} by XBOOLE_1:37, SSS;
then consider c being object such that
G9: c in X \ {a} by XBOOLE_0:def 1;
reconsider c = c as Element of TarskiEuclid2Space by G9;
su: X \ {a} c= X by XBOOLE_1:36;
set S = { j where j is Real : ( j >= 1 & (Tn2TR a) + (j * ((Tn2TR c) - (Tn2TR a))) in Y ) } ;
{ j where j is Real : ( j >= 1 & (Tn2TR a) + (j * ((Tn2TR c) - (Tn2TR a))) in Y ) } is real-membered

proof

let w be object ; :: according to MEMBERED:def 3 :: thesis:
assume w in { j where j is Real : ( j >= 1 & (Tn2TR a) + (j * ((Tn2TR c) - (Tn2TR a))) in Y ) } ; :: thesis:
then consider j1 being Real such that
G1: ( w = j1 & j1 >= 1 & (Tn2TR a) + (j1 * ((Tn2TR c) - (Tn2TR a))) in Y ) ;
thus w is real by G1; :: thesis:

end;

then reconsider S = { j where j is Real : ( j >= 1 & (Tn2TR a) + (j * ((Tn2TR c) - (Tn2TR a))) in Y ) } as real-membered set ;
gg: 1 is LowerBound of S

proof

let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis:
assume x in S ; :: thesis:
then consider j1 being Real such that
G1: ( x = j1 & j1 >= 1 & (Tn2TR a) + (j1 * ((Tn2TR c) - (Tn2TR a))) in Y ) ;
thus 1 <= x by G1; :: thesis:

end;

consider d being object such that
G2: d in Y by XBOOLE_0:def 1, SSS;
reconsider d = d as Element of TarskiEuclid2Space by G2;
Tn2TR c in LSeg ((Tn2TR a),(Tn2TR d)) by ThConv6, su, G9, A1, G2;
then consider jda being Real such that
G0: ( 0 <= jda & jda <= 1 & (Tn2TR c) - (Tn2TR a) = jda * ((Tn2TR d) - (Tn2TR a)) ) by ThConvAG;
set jd = 1 / jda;
hh: jda <> 0

proof

assume jda = 0 ; :: thesis:
then (Tn2TR c) - (Tn2TR a) = (0. (TOP-REAL 2)) + (0 * ((Tn2TR d) - (Tn2TR a))) by G0
.= 0. (TOP-REAL 2) by THJE ;
hence contradiction by G9, ZFMISC_1:56, RLVECT_1:21; :: thesis:

end;

Lem: for y being Element of TarskiEuclid2Space st y in Y holds
ex j1 being Real st
( j1 >= 1 & (Tn2TR y) - (Tn2TR a) = j1 * ((Tn2TR c) - (Tn2TR a)) )

proof

let y be Element of TarskiEuclid2Space; :: thesis:
assume y in Y ; :: thesis:
then Tn2TR c in LSeg ((Tn2TR a),(Tn2TR y)) by A1, su, G9, ThConv6;
then consider j being Real such that
H1: ( 0 <= j & j <= 1 & (Tn2TR c) - (Tn2TR a) = j * ((Tn2TR y) - (Tn2TR a)) ) by ThConvAG;
set j1 = 1 / j;
H2: j <> 0

proof

assume j = 0 ; :: thesis:
then (Tn2TR c) - (Tn2TR a) = (0. (TOP-REAL 2)) + (0 * ((Tn2TR y) - (Tn2TR a))) by H1
.= 0. (TOP-REAL 2) by THJE ;
hence contradiction by G9, ZFMISC_1:56, RLVECT_1:21; :: thesis:

end;

then H5: 1 / j >= 1 by H1, XREAL_1:181;
(1 / j) * ((Tn2TR c) - (Tn2TR a)) = ((1 / j) * j) * ((Tn2TR y) - (Tn2TR a)) by RLVECT_1:def 7, H1
.= 1 * ((Tn2TR y) - (Tn2TR a)) by H2, XCMPLX_0:def 7
.= (Tn2TR y) - (Tn2TR a) by RVSUM_1:52 ;
hence ex j1 being Real st
( j1 >= 1 & (Tn2TR y) - (Tn2TR a) = j1 * ((Tn2TR c) - (Tn2TR a)) ) by H5; :: thesis:

end;

Gy: (1 / jda) * ((Tn2TR c) - (Tn2TR a)) = ((1 / jda) * jda) * ((Tn2TR d) - (Tn2TR a)) by RLVECT_1:def 7, G0
.= 1 * ((Tn2TR d) - (Tn2TR a)) by hh, XCMPLX_0:def 7
.= (Tn2TR d) - (Tn2TR a) by RVSUM_1:52 ;
J2: 1 / jda >= 1 by XREAL_1:181, G0, hh;
((1 / jda) * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a) = (Tn2TR d) + ((- (Tn2TR a)) + (Tn2TR a)) by RLVECT_1:def 3, Gy
.= (Tn2TR d) + (0. (TOP-REAL 2)) by RLVECT_1:5 ;
then J1: 1 / jda in S by J2, G2;
reconsider S = S as non empty real-membered bounded_below set by J1, gg, XXREAL_2:def 9;
set k = inf S;
set bb = (Tn2TR a) + ((inf S) * ((Tn2TR c) - (Tn2TR a)));
p2: MetrStruct(# the U1 of TarskiEuclid2Space, the distance of TarskiEuclid2Space #) = MetrStruct(# the U1 of (Euclid 2), the distance of (Euclid 2) #) by GTARSKI1:def 13;
reconsider bb = (Tn2TR a) + ((inf S) * ((Tn2TR c) - (Tn2TR a))) as Element of TarskiEuclid2Space by p2, EUCLID:67;
ex b being Element of TarskiEuclid2Space st
for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between x,b,y

proof

take b = bb; :: thesis:
let x, y be Element of TarskiEuclid2Space; :: thesis:
assume T1: ( x in X & y in Y ) ; :: thesis:
then consider j1 being Real such that
HH: ( j1 >= 1 & (Tn2TR y) - (Tn2TR a) = j1 * ((Tn2TR c) - (Tn2TR a)) ) by Lem;
(Tn2TR y) + ((- (Tn2TR a)) + (Tn2TR a)) = (Tn2TR a) + (j1 * ((Tn2TR c) - (Tn2TR a))) by HH, RLVECT_1:def 3;
then hH: (Tn2TR y) + (0. (TOP-REAL 2)) = (Tn2TR a) + (j1 * ((Tn2TR c) - (Tn2TR a))) by RLVECT_1:5;
Tn2TR x in LSeg ((Tn2TR a),(Tn2TR d)) by T1, A1, G2, ThConv6;
then consider l being Real such that
z1: ( 0 <= l & l <= 1 & (Tn2TR x) - (Tn2TR a) = l * ((Tn2TR d) - (Tn2TR a)) ) by ThConvAG;
z2: (Tn2TR x) - (Tn2TR a) = (l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a)) by RLVECT_1:def 7, z1, Gy;
set i = l * (1 / jda);
(Tn2TR x) + ((- (Tn2TR a)) + (Tn2TR a)) = ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a) by z2, RLVECT_1:def 3;
then E3: (Tn2TR x) + (0. (TOP-REAL 2)) = ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a) by RLVECT_1:5;
for h being ExtReal st h in S holds
l * (1 / jda) <= h

proof

let h be ExtReal; :: thesis:
assume h in S ; :: thesis:
then consider j1 being Real such that
G1: ( h = j1 & j1 >= 1 & (Tn2TR a) + (j1 * ((Tn2TR c) - (Tn2TR a))) in Y ) ;
set z = (Tn2TR a) + (j1 * ((Tn2TR c) - (Tn2TR a)));
reconsider z = (Tn2TR a) + (j1 * ((Tn2TR c) - (Tn2TR a))) as Element of TarskiEuclid2Space by EUCLID:67, p2;
Tn2TR x in LSeg ((Tn2TR a),(Tn2TR z)) by T1, A1, G1, ThConv6;
then consider ll being Real such that
z1: ( 0 <= ll & ll <= 1 & (Tn2TR x) - (Tn2TR a) = ll * ((Tn2TR z) - (Tn2TR a)) ) by ThConvAG;
z0: (Tn2TR c) - (Tn2TR a) <> 0. (TOP-REAL 2)

proof

assume (Tn2TR c) - (Tn2TR a) = 0. (TOP-REAL 2) ; :: thesis:
then (Tn2TR c) + ((- (Tn2TR a)) + (Tn2TR a)) = (0. (TOP-REAL 2)) + (Tn2TR a) by RLVECT_1:def 3;
then (Tn2TR c) + (0. (TOP-REAL 2)) = (0. (TOP-REAL 2)) + (Tn2TR a) by RLVECT_1:5;
hence contradiction by G9, ZFMISC_1:56; :: thesis:

end;

(Tn2TR z) - (Tn2TR a) = (j1 * ((Tn2TR c) - (Tn2TR a))) + ((Tn2TR a) + (- (Tn2TR a))) by RLVECT_1:def 3
.= (j1 * ((Tn2TR c) - (Tn2TR a))) + (0. (TOP-REAL 2)) by RLVECT_1:5
.= j1 * ((Tn2TR c) - (Tn2TR a)) ;
then (Tn2TR x) - (Tn2TR a) = (ll * j1) * ((Tn2TR c) - (Tn2TR a)) by z1, RLVECT_1:def 7;
then ll * j1 = l * (1 / jda) by RLVECT_1:37, z0, z2;
hence l * (1 / jda) <= h by G1, XREAL_1:153, z1; :: thesis:

end;

then fF: l * (1 / jda) is LowerBound of S by XXREAL_2:def 2;
then f1: l * (1 / jda) <= inf S by XXREAL_2:def 4;
j1 in S by hH, HH, T1;
then F0: inf S <= j1 by XXREAL_2:3;
then f2: l * (1 / jda) <= j1 by f1, XXREAL_0:2;
ff: (Tn2TR b) - (Tn2TR x) = ((Tn2TR a) + ((inf S) * ((Tn2TR c) - (Tn2TR a)))) + ((- ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a)))) + (- (Tn2TR a))) by E3, RLVECT_1:31
.= ((((inf S) * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a)) + (- (Tn2TR a))) + (- ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a)))) by RLVECT_1:def 3
.= (((inf S) * ((Tn2TR c) - (Tn2TR a))) + ((Tn2TR a) + (- (Tn2TR a)))) + (- ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a)))) by RLVECT_1:def 3
.= (((inf S) * ((Tn2TR c) - (Tn2TR a))) + (0. (TOP-REAL 2))) + (- ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a)))) by RLVECT_1:5
.= ((inf S) * ((Tn2TR c) - (Tn2TR a))) - ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a)))
.= ((inf S) - (l * (1 / jda))) * ((Tn2TR c) - (Tn2TR a)) by RLVECT_1:35 ;
set l = ((inf S) - (l * (1 / jda))) / (j1 - (l * (1 / jda)));

per cases ;

suppose l * (1 / jda) = j1 ; :: thesis:

then inf S = l * (1 / jda) by F0, f1, XXREAL_0:1;
then (Tn2TR b) - (Tn2TR x) = (0. (TOP-REAL 2)) + (0 * ((Tn2TR c) - (Tn2TR a))) by ff
.= 0. (TOP-REAL 2) by THJE ;
then (Tn2TR b) + ((- (Tn2TR x)) + (Tn2TR x)) = (0. (TOP-REAL 2)) + (Tn2TR x) by RLVECT_1:def 3;
then (Tn2TR b) + (0. (TOP-REAL 2)) = (0. (TOP-REAL 2)) + (Tn2TR x) by RLVECT_1:5;
hence between x,b,y by GTARSKI1:17; :: thesis:

end;

suppose l * (1 / jda) <> j1 ; :: thesis:

then l * (1 / jda) < j1 by f2, XXREAL_0:1;
then R1: j1 - (l * (1 / jda)) > 0 by XREAL_1:50;
(Tn2TR y) - (Tn2TR x) = ((Tn2TR a) + (j1 * ((Tn2TR c) - (Tn2TR a)))) + ((- ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a)))) + (- (Tn2TR a))) by RLVECT_1:31, E3, hH
.= (((j1 * ((Tn2TR c) - (Tn2TR a))) + (Tn2TR a)) + (- (Tn2TR a))) - ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a))) by RLVECT_1:def 3
.= ((j1 * ((Tn2TR c) - (Tn2TR a))) + ((Tn2TR a) + (- (Tn2TR a)))) - ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a))) by RLVECT_1:def 3
.= ((j1 * ((Tn2TR c) - (Tn2TR a))) + (0. (TOP-REAL 2))) - ((l * (1 / jda)) * ((Tn2TR c) - (Tn2TR a))) by RLVECT_1:5
.= (j1 - (l * (1 / jda))) * ((Tn2TR c) - (Tn2TR a)) by RLVECT_1:35 ;
then (1 / (j1 - (l * (1 / jda)))) * ((Tn2TR y) - (Tn2TR x)) = ((1 / (j1 - (l * (1 / jda)))) * (j1 - (l * (1 / jda)))) * ((Tn2TR c) - (Tn2TR a)) by RLVECT_1:def 7;
then (1 / (j1 - (l * (1 / jda)))) * ((Tn2TR y) - (Tn2TR x)) = 1 * ((Tn2TR c) - (Tn2TR a)) by XCMPLX_0:def 7, R1;
then (Tn2TR c) - (Tn2TR a) = (1 / (j1 - (l * (1 / jda)))) * ((Tn2TR y) - (Tn2TR x)) by RVSUM_1:52;
then S2: (Tn2TR b) - (Tn2TR x) = (((inf S) - (l * (1 / jda))) / (j1 - (l * (1 / jda)))) * ((Tn2TR y) - (Tn2TR x)) by RLVECT_1:def 7, ff;
R4: (inf S) - (l * (1 / jda)) <= j1 - (l * (1 / jda)) by XREAL_1:13, F0;
(inf S) - (l * (1 / jda)) >= 0 by fF, XREAL_1:48, XXREAL_2:def 4;
then Tn2TR b in LSeg ((Tn2TR x),(Tn2TR y)) by S2, ThConvAGI, R4, XREAL_1:183;
hence between x,b,y by ThConv6; :: thesis:

end;

hence ex b being Element of TarskiEuclid2Space st
for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between x,b,y ; :: thesis:

end;