let n be 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 that
A1: P = LSeg (w1,w2) and
A2: 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)) ;
A3: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider Q = {(0. (TOP-REAL n))} as Subset of (TopSpaceMetr (Euclid n)) ;
P0 is compact by A1, A3, COMPTS_1:23;
then consider x1, x2 being Point of (Euclid n) such that
A4: x1 in P0 and
A5: x2 in Q and
A6: dist (x1,x2) = min_dist_min (P0,Q) by A1, A3, WEIERSTR:30;
reconsider w01 = x1 as Point of (TOP-REAL n) by EUCLID:67;
A7: x2 = 0. (TOP-REAL n) by A5, TARSKI:def 1;
reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
reconsider o2 = 0. (TOP-REAL n) as Point of (TopSpaceMetr (Euclid n)) by A3;
for x being object holds
( x in (dist_min P0) .: Q iff x = (dist_min P0) . o )

proof

let x be object ; :: 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 ex y being object st
( y in dom (dist_min P0) & y in Q & x = (dist_min P0) . y ) by FUNCT_1:def 6;
hence x = (dist_min P0) . o by TARSKI:def 1; :: thesis: verum

end;

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

end;

then A9: (dist_min P0) .: Q = {((dist_min P0) . o)} by TARSKI:def 1;
( [#] ((dist_min P0) .: Q) = (dist_min P0) .: Q & lower_bound ([#] ((dist_min P0) .: Q)) = lower_bound ((dist_min P0) .: Q) ) by WEIERSTR:def 1, WEIERSTR:def 3;
then A10: lower_bound ((dist_min P0) .: Q) = (dist_min P0) . o by A9, SEQ_4:9;
A11: |.w01.| = |.(w01 - (0. (TOP-REAL n))).| by RLVECT_1:13
.= dist (x1,x2) by A7, JGRAPH_1:28 ;
|.w01.| <> 0 by A1, A2, A4, TOPRNS_1:24;
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, A4, A6, A10, A11, WEIERSTR:def 7; :: thesis: verum