let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is Bounded holds
ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
let p, q be Point of (TOP-REAL n); :: thesis: for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is Bounded holds
ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
set TRn = TOP-REAL n;
let A be Subset of (TOP-REAL n); :: thesis: ( p in A & p <> q & A /\ (halfline (p,q)) is Bounded implies ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) ) )
assume that
A1: p in A and
A2: p <> q and
A3: A /\ (halfline (p,q)) is Bounded ; :: thesis: ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
reconsider P = p, Q = q as Element of (Euclid n) by EUCLID:67;
A4: dist (P,Q) > 0 by A2, METRIC_1:7;
set H = halfline (p,q);
reconsider AH = A /\ (halfline (p,q)) as bounded Subset of (Euclid n) by A3, JORDAN2C:def 1;
A5: n in NAT by ORDINAL1:def 12;
then A6: dist (Q,P) = |.(q - p).| by SPPOL_1:39;
p in halfline (p,q) by A5, TOPREAL9:27;
then A7: p in AH by A1, XBOOLE_0:def 4;
set DAH = diameter AH;
set X = { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } ;
set dAH = (diameter AH) + 1;

A8: now

let x be set ; :: thesis: ( x in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } implies x is real )
assume x in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } ; :: thesis: x is real
then ex r being Real st
( x = r & ((1 - r) * p) + (r * q) in AH & 0 <= r ) ;
hence x is real ; :: thesis: verum

end;

( 1 * p = p & 0 * q = 0. (TOP-REAL n) ) by RLVECT_1:10, RLVECT_1:def 8;
then p = ((1 - 0) * p) + (0 * q) by RLVECT_1:def 4;
then A9: 0 in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } by A7;
then reconsider X = { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } as non empty real-membered set by A8, MEMBERED:def 3;
A10: (diameter AH) + 0 < (diameter AH) + 1 by XREAL_1:8;

now

let x be ext-real number ; :: thesis: ( x in X implies x <= ((diameter AH) + 1) / (dist (Q,P)) )
assume x in X ; :: thesis: x <= ((diameter AH) + 1) / (dist (Q,P))
then consider r being Real such that
A11: x = r and
A12: ((1 - r) * p) + (r * q) in AH and
A13: 0 <= r ;
reconsider PQ = ((1 - r) * p) + (r * q) as Element of (Euclid n) by A12;
(((1 - r) * p) + (r * q)) - p = r * (q - p) by Lm1;
then dist (PQ,P) = |.(r * (q - p)).| by A5, SPPOL_1:39
.= (abs r) * |.(q - p).| by A5, TOPRNS_1:7
.= r * (dist (Q,P)) by A6, A13, ABSVALUE:def 1 ;
then r * (dist (Q,P)) <= diameter AH by A7, A12, TBSP_1:def 8;
then A14: r * (dist (Q,P)) <= (diameter AH) + 1 by A10, XXREAL_0:2;
(r * (dist (Q,P))) / (dist (Q,P)) = r * ((dist (Q,P)) / (dist (Q,P)))
.= r * 1 by A4, XCMPLX_1:60 ;
hence x <= ((diameter AH) + 1) / (dist (Q,P)) by A11, A14, XREAL_1:72; :: thesis: verum

end;

then ((diameter AH) + 1) / (dist (P,Q)) is UpperBound of X by XXREAL_2:def 1;
then X is bounded_above by XXREAL_2:def 10;
then reconsider S = sup X as Real by XXREAL_2:16;
A15: 0 <= S by A9, XXREAL_2:4;
set Spq = ((1 - S) * p) + (S * q);
reconsider spq = ((1 - S) * p) + (S * q) as Element of (Euclid n) by EUCLID:67;
A16: for r being real number st r > 0 holds
ex w being Point of (Euclid n) st
( w in AH & dist (spq,w) < r )

proof

let r be real number ; :: thesis: ( r > 0 implies ex w being Point of (Euclid n) st
( w in AH & dist (spq,w) < r ) )
assume A17: r > 0 ; :: thesis: ex w being Point of (Euclid n) st
( w in AH & dist (spq,w) < r )
set r2 = r / |.(q - p).|;
assume A18: for w being Point of (Euclid n) st w in AH holds
dist (spq,w) >= r ; :: thesis: contradiction

now

let x be ext-real number ; :: thesis: ( x in X implies S - (r / |.(q - p).|) >= x )
assume A19: x in X ; :: thesis: S - (r / |.(q - p).|) >= x
then consider w being Real such that
A20: x = w and
A21: ((1 - w) * p) + (w * q) in AH and
0 <= w ;
S - w >= 0 by A19, A20, XREAL_1:48, XXREAL_2:4;
then A22: abs (S - w) = S - w by ABSVALUE:def 1;
reconsider PQ = ((1 - w) * p) + (w * q) as Element of (Euclid n) by A21;
A23: PQ = p + (w * (q - p)) by Th1;
(((1 - S) * p) + (S * q)) - (p + (w * (q - p))) = ((((1 - S) * p) + (S * q)) - p) - (w * (q - p)) by RLVECT_1:27
.= (S * (q - p)) - (w * (q - p)) by Lm1
.= (S - w) * (q - p) by RLVECT_1:35 ;
then dist (spq,PQ) = |.((S - w) * (q - p)).| by A5, A23, SPPOL_1:39
.= (S - w) * |.(q - p).| by A5, A22, TOPRNS_1:7 ;
then (S - w) * |.(q - p).| >= r by A18, A21;
then S - w >= r / |.(q - p).| by A2, A6, METRIC_1:7, XREAL_1:79;
hence S - (r / |.(q - p).|) >= x by A20, XREAL_1:11; :: thesis: verum

end;

then S - (r / |.(q - p).|) is UpperBound of X by XXREAL_2:def 1;
then S - 0 <= S - (r / |.(q - p).|) by XXREAL_2:def 3;
hence contradiction by A4, A6, A17, XREAL_1:8; :: thesis: verum

end;

A24: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

now

let U be Subset of (TOP-REAL n); :: thesis: ( U is open & ((1 - S) * p) + (S * q) in U implies ( A meets U & U \ A <> {} ) )
reconsider UE = U as Subset of (TopSpaceMetr (Euclid n)) by A24;
assume that
A25: U is open and
A26: ((1 - S) * p) + (S * q) in U ; :: thesis: ( A meets U & U \ A <> {} )
UE in the topology of (TopSpaceMetr (Euclid n)) by A24, A25, PRE_TOPC:def 2;
then UE is open by PRE_TOPC:def 2;
then consider r being real number such that
A27: r > 0 and
A28: Ball (spq,r) c= UE by A26, TOPMETR:15;
set r2 = r / |.(q - p).|;
set Sr = S + ((r / |.(q - p).|) / 2);
consider w being Element of (Euclid n) such that
A29: ( w in AH & dist (spq,w) < r ) by A16, A27;
( w in Ball (spq,r) & w in A ) by A29, METRIC_1:11, XBOOLE_0:def 4;
hence A meets U by A28, XBOOLE_0:3; :: thesis: U \ A <> {}
A30: (r / |.(q - p).|) * |.(q - p).| = r * (|.(q - p).| / |.(q - p).|)
.= r * 1 by A4, A6, XCMPLX_1:60 ;
S + ((r / |.(q - p).|) / 2) > S + 0 by A4, A6, A27, XREAL_1:6;
then S - (S + ((r / |.(q - p).|) / 2)) < 0 by XREAL_1:49;
then A31: abs (S - (S + ((r / |.(q - p).|) / 2))) = - (S - (S + ((r / |.(q - p).|) / 2))) by ABSVALUE:def 1
.= (r / |.(q - p).|) / 2 ;
set Srpq = ((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q);
reconsider srpq = ((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q) as Element of (Euclid n) by EUCLID:67;
A32: srpq in halfline (p,q) by A15, A27;
A33: not srpq in A

proof

assume srpq in A ; :: thesis: contradiction
then srpq in AH by A32, XBOOLE_0:def 4;
then S + ((r / |.(q - p).|) / 2) in X by A15, A27;
then S + ((r / |.(q - p).|) / 2) <= S + 0 by XXREAL_2:4;
hence contradiction by A4, A6, A27, XREAL_1:8; :: thesis: verum

end;

(((1 - S) * p) + (S * q)) - (((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q)) = (((1 - S) * p) + (S * q)) - (p + ((S + ((r / |.(q - p).|) / 2)) * (q - p))) by Th1
.= ((((1 - S) * p) + (S * q)) - p) - ((S + ((r / |.(q - p).|) / 2)) * (q - p)) by RLVECT_1:27
.= (S * (q - p)) - ((S + ((r / |.(q - p).|) / 2)) * (q - p)) by Lm1
.= (S - (S + ((r / |.(q - p).|) / 2))) * (q - p) by RLVECT_1:35 ;
then dist (spq,srpq) = |.((S - (S + ((r / |.(q - p).|) / 2))) * (q - p)).| by A5, SPPOL_1:39
.= ((r / |.(q - p).|) / 2) * |.(q - p).| by A5, A31, TOPRNS_1:7
.= r / 2 by A30 ;
then dist (spq,srpq) < r by A27, XREAL_1:216;
then srpq in Ball (spq,r) by METRIC_1:11;
hence U \ A <> {} by A28, A33, XBOOLE_0:def 5; :: thesis: verum

end;

then A34: ((1 - S) * p) + (S * q) in Fr A by TOPGEN_1:9;
take spq ; :: thesis: ( spq in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,spq) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) ) )
A35: (((1 - S) * p) + (S * q)) - p = S * (q - p) by Lm1;
((1 - S) * p) + (S * q) in halfline (p,q) by A15;
hence spq in (Fr A) /\ (halfline (p,q)) by A34, XBOOLE_0:def 4; :: thesis: ( ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,spq) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) ) )
A36: abs S = S by A15, ABSVALUE:def 1;

hereby :: thesis: for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r )

let u, P be Point of (Euclid n); :: thesis: ( P = p & u in A /\ (halfline (p,q)) implies dist (P,u) <= dist (P,spq) )
assume that
A37: P = p and
A38: u in A /\ (halfline (p,q)) ; :: thesis: dist (P,u) <= dist (P,spq)
A39: dist (P,spq) = |.(S * (q - p)).| by A5, A35, A37, SPPOL_1:39
.= S * |.(q - p).| by A5, A36, TOPRNS_1:7 ;
u in halfline (p,q) by A38, XBOOLE_0:def 4;
then consider Ur being real number such that
A40: u = ((1 - Ur) * p) + (Ur * q) and
A41: 0 <= Ur by A5, TOPREAL9:26;
A42: abs Ur = Ur by A41, ABSVALUE:def 1;
Ur in REAL by XREAL_0:def 1;
then Ur in X by A38, A40, A41;
then A43: Ur <= S by XXREAL_2:4;
set du = dist (P,u);
set ds = dist (P,spq);
A44: (((1 - Ur) * p) + (Ur * q)) - p = Ur * (q - p) by Lm1;
dist (P,u) = |.(Ur * (q - p)).| by A5, A37, A40, A44, SPPOL_1:39
.= Ur * |.(q - p).| by A5, A42, TOPRNS_1:7 ;
hence dist (P,u) <= dist (P,spq) by A39, A43, XREAL_1:64; :: thesis: verum

end;

thus for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) by A16; :: thesis: verum