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 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 st
( r > 0 & Ball (p,r) c= (dist_max X) " P ) )
set y = upper_bound ((dist p) .: X);
upper_bound ((dist p) .: X) in REAL by XREAL_0:def 1;
then reconsider y = upper_bound ((dist p) .: X) as Point of RealSpace by METRIC_1:def 13;
assume p in (dist_max X) " P ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= (dist_max X) " P )
then A3: (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 A3, Def5;
then consider r being Real such that
A4: r > 0 and
A5: 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_max X) " P )
Ball (p,r) c= (dist_max X) " P

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball (p,r) or z in (dist_max X) " P )
assume A6: z in Ball (p,r) ; :: thesis: z in (dist_max X) " P
then reconsider z = z as Point of M ;
set q = upper_bound ((dist z) .: X);
upper_bound ((dist z) .: X) in REAL by XREAL_0:def 1;
then reconsider q = upper_bound ((dist z) .: X) as Point of RealSpace by METRIC_1:def 13;
dist (p,z) < r by A6, METRIC_1:11;
then |.((upper_bound ((dist p) .: X)) - (upper_bound ((dist z) .: X))).| + (dist (p,z)) < r + (dist (p,z)) by A1, Th20, XREAL_1:8;
then |.((upper_bound ((dist p) .: X)) - (upper_bound ((dist z) .: X))).| < r by XREAL_1:6;
then dist (y,q) < r by TOPMETR:11;
then A7: q in Ball (y,r) by METRIC_1:11;
dom (dist_max X) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then A8: dom (dist_max X) = the carrier of M by TOPMETR:12;
q = (dist_max X) . z by Def5;
hence z in (dist_max X) " P by A5, A7, A8, FUNCT_1:def 7; :: thesis: verum

end;

hence ( r > 0 & Ball (p,r) c= (dist_max X) " P ) by A4; :: 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