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 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)) ;
LSeg w1,w2 is compact by SPPOL_1:28;
then P0 is compact by A1, A3, COMPTS_1:33;
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:36;
reconsider w01 = x1 as Point of (TOP-REAL n) by EUCLID:71;
A7: x2 = 0. (TOP-REAL n) by A5, TARSKI:def 1;
reconsider o = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:71;
reconsider o2 = 0. (TOP-REAL n) as Point of (TopSpaceMetr (Euclid n)) by A3;
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 ex y being set st
( y in dom (dist_min P0) & y in Q & x = (dist_min P0) . y ) by FUNCT_1:def 12;
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 12; :: 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 3, WEIERSTR:def 5;
then A10: lower_bound ((dist_min P0) .: Q) = (dist_min P0) . o by A9, SEQ_4:22;
A11: |.w01.| = |.(w01 - (0. (TOP-REAL n))).| by RLVECT_1:26
.= dist x1,x2 by A7, JGRAPH_1:45 ;
|.w01.| <> 0 by A1, A2, A4, 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, A4, A6, A10, A11, WEIERSTR:def 9; :: thesis: verum