let n be Element of NAT ; :: thesis: for w1, w2 being Point of (TOP-REAL n)
for P being Subset of (TopSpaceMetr (Euclid n)) st P = LSeg w1,w2 & not 0.REAL n in LSeg w1,w2 holds
ex w0 being Point of (TOP-REAL n) st
( w0 in LSeg w1,w2 & |.w0.| > 0 & |.w0.| = (dist_min P) . (0.REAL n) )
let w1, w2 be Point of (TOP-REAL n); :: thesis: for P being Subset of (TopSpaceMetr (Euclid n)) st P = LSeg w1,w2 & not 0.REAL n in LSeg w1,w2 holds
ex w0 being Point of (TOP-REAL n) st
( w0 in LSeg w1,w2 & |.w0.| > 0 & |.w0.| = (dist_min P) . (0.REAL n) )
let P be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( P = LSeg w1,w2 & not 0.REAL n in LSeg w1,w2 implies ex w0 being Point of (TOP-REAL n) st
( w0 in LSeg w1,w2 & |.w0.| > 0 & |.w0.| = (dist_min P) . (0.REAL n) ) )
assume A1: ( P = LSeg w1,w2 & not 0.REAL n in LSeg w1,w2 ) ; :: thesis: ex w0 being Point of (TOP-REAL n) st
( w0 in LSeg w1,w2 & |.w0.| > 0 & |.w0.| = (dist_min P) . (0.REAL n) )
set M = Euclid n;
reconsider P0 = P as Subset of (TopSpaceMetr (Euclid n)) ;
reconsider o = 0.REAL n as Point of (Euclid n) ;
reconsider o2 = 0.REAL n as Point of (TopSpaceMetr (Euclid n)) ;
A2: P0 is compact by A1, SPPOL_1:28;
reconsider Q = {(0.REAL n)} as Subset of (TopSpaceMetr (Euclid n)) ;
consider x1, x2 being Point of (Euclid n) such that
A3: ( x1 in P0 & x2 in Q & dist x1,x2 = min_dist_min P0,Q ) by A1, A2, WEIERSTR:36;
A4: for x being set holds
( x in (dist_min P0) .: Q iff x = (dist_min P0) . o )

proof

let x be set ; :: thesis: ( x in (dist_min P0) .: Q iff x = (dist_min P0) . o )

hereby :: thesis: ( x = (dist_min P0) . o implies x in (dist_min P0) .: Q )

assume x in (dist_min P0) .: Q ; :: thesis: x = (dist_min P0) . o
then consider y being set such that
A5: ( y in dom (dist_min P0) & y in Q & x = (dist_min P0) . y ) by FUNCT_1:def 12;
thus x = (dist_min P0) . o by A5, TARSKI:def 1; :: thesis: verum

end;

assume A6: x = (dist_min P0) . o ; :: thesis: x in (dist_min P0) .: Q
A7: o in Q by TARSKI:def 1;
o2 in the carrier of (TopSpaceMetr (Euclid n)) ;
then o in dom (dist_min P0) by FUNCT_2:def 1;
hence x in (dist_min P0) .: Q by A6, A7, FUNCT_1:def 12; :: thesis: verum

end;

A8: [#] ((dist_min P0) .: Q) = (dist_min P0) .: Q by WEIERSTR:def 3;
A9: (dist_min P0) .: Q = {((dist_min P0) . o)} by A4, TARSKI:def 1;
lower_bound ([#] ((dist_min P0) .: Q)) = lower_bound ((dist_min P0) .: Q) by WEIERSTR:def 5;
then A10: lower_bound ((dist_min P0) .: Q) = (dist_min P0) . o by A8, A9, SEQ_4:22;
A11: x2 = 0.REAL n by A3, TARSKI:def 1;
reconsider w01 = x1 as Point of (TOP-REAL n) by A3;
A12: |.w01.| = |.(w01 - (0.REAL n)).| by Th13
.= dist x1,x2 by A11, JGRAPH_1:45 ;
|.w01.| <> 0 by A1, A3, TOPRNS_1:25;
hence ex w0 being Point of (TOP-REAL n) st
( w0 in LSeg w1,w2 & |.w0.| > 0 & |.w0.| = (dist_min P) . (0.REAL n) ) by A1, A3, A10, A12, WEIERSTR:def 9; :: thesis: verum