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

proof

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

proof

let p be Point of M; :: thesis: ( p in (dist_max X) " P implies ex r being real number st
( r > 0 & Ball (p,r) c= (dist_max X) " P ) )
consider y being Point of RealSpace such that
A3: y = upper_bound ((dist p) .: X) by METRIC_1:def 13;
assume p in (dist_max X) " P ; :: thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (dist_max X) " P )
then A4: (dist_max X) . p in P by FUNCT_1:def 7;
reconsider P = P as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def 6;
y in P by A4, A3, Def7;
then consider r being real number such that
A5: r > 0 and
A6: 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_max X) " P )
Ball (p,r) c= (dist_max X) " P

proof

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

end;

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

end;

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

end;

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