let M be non empty MetrSpace; :: thesis: for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds
dist_min X is continuous
let X be Subset of (TopSpaceMetr M); :: thesis: ( X <> {} & X is compact implies dist_min X is continuous )
assume A1: ( X <> {} & X is compact ) ; :: thesis: dist_min X is continuous
for P being Subset of R^1 st P is open holds
(dist_min X) " P is open

proof

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

proof

let p be Point of M; :: thesis: ( p in (dist_min X) " P implies ex r being real number st
( r > 0 & Ball (p,r) c= (dist_min X) " P ) )
assume A3: p in (dist_min X) " P ; :: thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (dist_min X) " P )
ex r being Real st
( r > 0 & Ball (p,r) c= (dist_min X) " P )

proof

A4: (dist_min X) . p in P by A3, FUNCT_1:def 7;
reconsider P = P as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def 6;
consider y being Point of RealSpace such that
A5: y = lower_bound ((dist p) .: X) by METRIC_1:def 13;
y in P by A4, A5, Def8;
then consider r being real number such that
A6: r > 0 and
A7: Ball (y,r) c= P by A2, TOPMETR:15, TOPMETR:def 6;
reconsider r = r as Real by XREAL_0:def 1;
take r ; :: thesis: ( r > 0 & Ball (p,r) c= (dist_min X) " P )
Ball (p,r) c= (dist_min X) " P

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball (p,r) or z in (dist_min X) " P )
assume A8: z in Ball (p,r) ; :: thesis: z in (dist_min X) " P
then reconsider z = z as Point of M ;
consider q being Point of RealSpace such that
A9: q = lower_bound ((dist z) .: X) by METRIC_1:def 13;
dist (p,z) < r by A8, METRIC_1:11;
then (abs ((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X)))) + (dist (p,z)) < r + (dist (p,z)) by A1, Th28, XREAL_1:8;
then abs ((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X))) < r by XREAL_1:6;
then dist (y,q) < r by A5, A9, TOPMETR:11;
then A10: q in Ball (y,r) by METRIC_1:11;
dom (dist_min X) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then A11: dom (dist_min X) = the carrier of M by TOPMETR:12;
q = (dist_min X) . z by A9, Def8;
hence z in (dist_min X) " P by A7, A10, A11, FUNCT_1:def 7; :: thesis: verum

end;

hence ( r > 0 & Ball (p,r) c= (dist_min X) " P ) by A6; :: thesis: verum

end;

hence ex r being real number st
( r > 0 & Ball (p,r) c= (dist_min X) " P ) ; :: thesis: verum

end;

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

end;

hence dist_min X is continuous by Lm2, TOPS_2:43; :: thesis: verum