let X, Y be Subset of TarskiEuclid2Space; ( ex a being Element of TarskiEuclid2Space st
for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between a,x,y implies 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 )
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
; 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
per cases
( X c= {a} or Y = {} or ( not X c= {a} & Y <> {} ) )
;
suppose SS:
(
X c= {a} or
Y = {} )
;
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
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;
for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between x,b,y
let x,
y be
Element of
TarskiEuclid2Space;
( x in X & y in Y implies between x,b,y )
assume
(
x in X &
y in Y )
;
between x,b,y
then
x = a
by SS, TARSKI:def 1;
hence
between x,
b,
y
by GTARSKI1:17;
verum
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
;
verum end; suppose SSS:
( not
X c= {a} &
Y <> {} )
;
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
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
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
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
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)) )
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;
for x, y being Element of TarskiEuclid2Space st x in X & y in Y holds
between x,b,y
let x,
y be
Element of
TarskiEuclid2Space;
( x in X & y in Y implies between x,b,y )
assume T1:
(
x in X &
y in Y )
;
between x,b,y
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;
( h in S implies l * (1 / jda) <= h )
assume
h in S
;
l * (1 / jda) <= h
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)
(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;
verum
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
( l * (1 / jda) = j1 or l * (1 / jda) <> j1 )
;
suppose
l * (1 / jda) <> j1
;
between x,b,ythen
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;
verum end; end;
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
;
verum end; end;