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. (TOP-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. (TOP-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. (TOP-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. (TOP-REAL n)) )
let P be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( P = LSeg w1,w2 & not 0. (TOP-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. (TOP-REAL n)) ) )
assume A1: ( P = LSeg w1,w2 & not 0. (TOP-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. (TOP-REAL n)) )
set M = Euclid n;
reconsider P0 = P as Subset of (TopSpaceMetr (Euclid n)) ;
U: the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:71;
then reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by XX, YY;
V: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider o2 = 0. (TOP-REAL n) as Point of (TopSpaceMetr (Euclid n)) by XX, YY, U;
LSeg w1,w2 is compact by A1, SPPOL_1:28;
then A2: P0 is compact by A1, V, COMPTS_1:33;
reconsider Q = {(0. (TOP-REAL n))} as Subset of (TopSpaceMetr (Euclid n)) by XX, YY, U, V;
{(0. (TOP-REAL n))} is compact ;
then Q is compact by V, COMPTS_1:33;
then 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)) by XX, YY, V;
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. (TOP-REAL n) by A3, TARSKI:def 1;
the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:71;
then reconsider w01 = x1 as Point of (TOP-REAL n) by A3, XX, YY;
A12: |.w01.| = |.(w01 - (0. (TOP-REAL n))).| by RLVECT_1:26, RLVECT_1:27
.= 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. (TOP-REAL n)) ) by A1, A3, A10, A12, WEIERSTR:def 9; :: thesis: verum