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 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 6;
let p be Point of M; :: thesis: ( p in (dist_min A) " P implies ex r being Real st
( r > 0 & Ball (p,r) c= (dist_min A) " P ) )
assume p in (dist_min A) " P ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= (dist_min A) " P )
then A3: (dist_min A) . p in P by FUNCT_1:def 7;
then reconsider dp = (dist_min A) . p as Point of RealSpace by TOPMETR:def 6;
consider r being Real such that
A4: r > 0 and
A5: Ball (dp,r) c= P9 by A3, TOPMETR:15;
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 object ; :: 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:11;
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 3;
then reconsider dq = (dist_min A) . q as Point of RealSpace by TOPMETR:def 6;
(dist_min A) . q <= (dist (q,p)) + ((dist_min A) . p) by HAUSDORF:15;
then ((dist_min A) . q) - ((dist_min A) . p) <= dist (p,q) by XREAL_1:20;
then A9: - (dist (p,q)) <= - (((dist_min A) . q) - ((dist_min A) . p)) by XREAL_1:24;
(dist_min A) . p <= (dist (p,q)) + ((dist_min A) . q) by HAUSDORF:15;
then ((dist_min A) . p) - ((dist_min A) . q) <= dist (p,q) by XREAL_1:20;
then |.(((dist_min A) . p) - ((dist_min A) . q)).| <= dist (p,q) by A9, ABSVALUE:5;
then |.(((dist_min A) . p) - ((dist_min A) . q)).| < r by A7, XXREAL_0:2;
then dist (dp,dq) < r by METRIC_1:def 12;
then dq in Ball (dp,r) by METRIC_1:11;
hence x in (dist_min A) " P by A5, A8, FUNCT_1:def 7; :: thesis: verum

end;

end;

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

end;

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