set d = dist_min A;
set TM = TopSpaceMetr M;
A1: for P being Subset of R^1 st P is open holds
(dist_min A) " P is open

proof

let P be Subset of R^1 ; :: thesis: ( P is open implies (dist_min A) " P is open )
assume A2: P is open ; :: thesis: (dist_min A) " P is open
for p being Point of M st p in (dist_min A) " P holds
ex r being real number st
( r > 0 & Ball p,r c= (dist_min A) " P )

proof

reconsider P9 = P as open Subset of (TopSpaceMetr RealSpace ) by A2, TOPMETR:def 7;
let p be Point of M; :: thesis: ( p in (dist_min A) " P implies ex r being real number st
( r > 0 & Ball p,r c= (dist_min A) " P ) )
assume p in (dist_min A) " P ; :: thesis: ex r being real number st
( r > 0 & Ball p,r c= (dist_min A) " P )
then A3: (dist_min A) . p in P by FUNCT_1:def 13;
then reconsider dp = (dist_min A) . p as Point of RealSpace by TOPMETR:def 7;
consider r being real number such that
A4: r > 0 and
A5: Ball dp,r c= P9 by A3, TOPMETR:22;
take r ; :: thesis: ( r > 0 & Ball p,r c= (dist_min A) " P )
thus r > 0 by A4; :: thesis: Ball p,r c= (dist_min A) " P
thus Ball p,r c= (dist_min A) " P :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball p,r or x in (dist_min A) " P )
assume A6: x in Ball p,r ; :: thesis: x in (dist_min A) " P
then reconsider q = x as Point of M ;
A7: dist p,q < r by A6, METRIC_1:12;
A8: dom (dist_min A) = [#] M by FUNCT_2:def 1;
then (dist_min A) . q in rng (dist_min A) by FUNCT_1:def 5;
then reconsider dq = (dist_min A) . q as Point of RealSpace by TOPMETR:def 7;
(dist_min A) . q <= (dist q,p) + ((dist_min A) . p) by HAUSDORF:17;
then ((dist_min A) . q) - ((dist_min A) . p) <= dist p,q by XREAL_1:22;
then A9: - (dist p,q) <= - (((dist_min A) . q) - ((dist_min A) . p)) by XREAL_1:26;
(dist_min A) . p <= (dist p,q) + ((dist_min A) . q) by HAUSDORF:17;
then ((dist_min A) . p) - ((dist_min A) . q) <= dist p,q by XREAL_1:22;
then abs (((dist_min A) . p) - ((dist_min A) . q)) <= dist p,q by A9, ABSVALUE:12;
then abs (((dist_min A) . p) - ((dist_min A) . q)) < r by A7, XXREAL_0:2;
then dist dp,dq < r by METRIC_1:def 13;
then dq in Ball dp,r by METRIC_1:12;
hence x in (dist_min A) " P by A5, A8, FUNCT_1:def 13; :: thesis: verum

end;

end;

hence (dist_min A) " P is open by TOPMETR:22; :: thesis: verum

end;

( [#] R^1 = {} implies [#] (TopSpaceMetr M) = {} ) ;
hence dist_min A is continuous by A1, TOPS_2:55; :: thesis: verum