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 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 st
( r > 0 & Ball (p,r) c= (dist_min X) " P ) )
assume A3: p in (dist_min X) " P ; :: thesis: ex r being Real 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;
set y = lower_bound ((dist p) .: X);
lower_bound ((dist p) .: X) in REAL by XREAL_0:def 1;
then reconsider y = lower_bound ((dist p) .: X) as Point of RealSpace by METRIC_1:def 13;
y in P by A4, Def6;
then consider r being Real such that
A5: r > 0 and
A6: Ball (y,r) c= P by A2, TOPMETR:15, TOPMETR:def 6;
reconsider r = r as Real ;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball (p,r) or z in (dist_min X) " P )
assume A7: z in Ball (p,r) ; :: thesis: z in (dist_min X) " P
then reconsider z = z as Point of M ;
set q = lower_bound ((dist z) .: X);
lower_bound ((dist z) .: X) in REAL by XREAL_0:def 1;
then reconsider q = lower_bound ((dist z) .: X) as Point of RealSpace by METRIC_1:def 13;
dist (p,z) < r by A7, METRIC_1:11;
then |.((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X))).| + (dist (p,z)) < r + (dist (p,z)) by A1, Th22, XREAL_1:8;
then |.((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X))).| < r by XREAL_1:6;
then dist (y,q) < r by TOPMETR:11;
then A8: q in Ball (y,r) by METRIC_1:11;
dom (dist_min X) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then A9: dom (dist_min X) = the carrier of M by TOPMETR:12;
q = (dist_min X) . z by Def6;
hence z in (dist_min X) " P by A6, A8, A9, FUNCT_1:def 7; :: thesis: verum

end;

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

end;

hence ex r being Real 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