let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for S being Subset of (TOP-REAL n) st p in S & p <> q & S /\ (halfline (p,q)) is bounded holds
ex w being Point of (TOP-REAL n) st
( w in (Fr S) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being Real st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in S /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
let p, q be Point of (TOP-REAL n); :: thesis: for S being Subset of (TOP-REAL n) st p in S & p <> q & S /\ (halfline (p,q)) is bounded holds
ex w being Point of (TOP-REAL n) st
( w in (Fr S) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being Real st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in S /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
set T = TOP-REAL n;
set E = Euclid 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 (TOP-REAL n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being Real st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) ) )
assume A1: ( p in A & p <> q & A /\ (halfline (p,q)) is bounded ) ; :: thesis: ex w being Point of (TOP-REAL n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being Real st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
consider W being Point of (Euclid n) such that
A2: W in (Fr A) /\ (halfline (p,q)) and
A3: for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,W) and
A4: for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (W,u) < r ) by A1, Lm3;
reconsider w = W as Point of (TOP-REAL n) by EUCLID:67;
take w ; :: thesis: ( w in (Fr A) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being Real st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
thus w in (Fr A) /\ (halfline (p,q)) by A2; :: thesis: ( ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being Real st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
reconsider P = p as Point of (Euclid n) by EUCLID:67;
hereby :: thesis: for r being Real st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r )
let u be Point of (TOP-REAL n); :: thesis: ( u in A /\ (halfline (p,q)) implies |.(p - u).| <= |.(p - w).| )
assume A5: u in A /\ (halfline (p,q)) ; :: thesis: |.(p - u).| <= |.(p - w).|
reconsider U = u as Point of (Euclid n) by EUCLID:67;
A6: dist (P,U) = |.(p - u).| by SPPOL_1:39;
dist (P,U) <= dist (P,W) by A3, A5;
hence |.(p - u).| <= |.(p - w).| by A6, SPPOL_1:39; :: thesis: verum
end;
let r be Real; :: thesis: ( r > 0 implies ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) )
assume r > 0 ; :: thesis: ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r )
then consider U being Point of (Euclid n) such that
A7: ( U in A /\ (halfline (p,q)) & dist (W,U) < r ) by A4;
reconsider u = U as Point of (TOP-REAL n) by EUCLID:67;
dist (W,U) = |.(w - u).| by SPPOL_1:39;
hence ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) by A7; :: thesis: verum