let M be non empty MetrSpace; :: thesis: for P, Q, R being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & R is compact holds
max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R))
let P, Q, R be non empty Subset of (TopSpaceMetr M); :: thesis: ( P is compact & Q is compact & R is compact implies max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume that
A1: P is compact and
A2: Q is compact and
A3: R is compact ; :: thesis: max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R))
reconsider DPR = (dist_min R) .: P as non empty Subset of REAL by TOPMETR:17;
A4: for w being Real st w in DPR holds
w <= (HausDist (P,Q)) + (HausDist (Q,R))

proof

let w be Real; :: thesis: ( w in DPR implies w <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume w in DPR ; :: thesis: w <= (HausDist (P,Q)) + (HausDist (Q,R))
then consider y being object such that
y in dom (dist_min R) and
A5: y in P and
A6: w = (dist_min R) . y by FUNCT_1:def 6;
reconsider y = y as Point of M by A5, TOPMETR:12;
for z being Point of M st z in Q holds
dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R))

proof

let z be Point of M; :: thesis: ( z in Q implies dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R)) )
assume z in Q ; :: thesis: dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R))
then (dist_min R) . z <= HausDist (Q,R) by A2, A3, Th32;
then A7: (dist (y,z)) + ((dist_min R) . z) <= (dist (y,z)) + (HausDist (Q,R)) by XREAL_1:6;
(dist_min R) . y <= (dist (y,z)) + ((dist_min R) . z) by Th15;
then (dist_min R) . y <= (dist (y,z)) + (HausDist (Q,R)) by A7, XXREAL_0:2;
hence dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R)) by XREAL_1:20; :: thesis: verum

end;

then A8: ((dist_min R) . y) - (HausDist (Q,R)) <= (dist_min Q) . y by Th14;
(dist_min Q) . y <= HausDist (P,Q) by A1, A2, A5, Th32;
then ((dist_min R) . y) - (HausDist (Q,R)) <= HausDist (P,Q) by A8, XXREAL_0:2;
hence w <= (HausDist (P,Q)) + (HausDist (Q,R)) by A6, XREAL_1:20; :: thesis: verum

end;

upper_bound DPR = upper_bound ([#] ((dist_min R) .: P)) by WEIERSTR:def 1
.= upper_bound ((dist_min R) .: P) by WEIERSTR:def 2
.= max_dist_min (R,P) by WEIERSTR:def 8 ;
hence max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R)) by A4, SEQ_4:45; :: thesis: verum