let M be non empty MetrSpace; :: thesis: for Q, R being non empty Subset of (TopSpaceMetr M)
for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= HausDist Q,R
let Q, R be non empty Subset of (TopSpaceMetr M); :: thesis: for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= HausDist Q,R
let y be Point of M; :: thesis: ( Q is compact & R is compact & y in Q implies (dist_min R) . y <= HausDist Q,R )
assume ( Q is compact & R is compact & y in Q ) ; :: thesis: (dist_min R) . y <= HausDist Q,R
then ( max_dist_min R,Q <= max (max_dist_min R,Q),(max_dist_min Q,R) & (dist_min R) . y <= max_dist_min R,Q ) by Th33, XXREAL_0:25;
hence (dist_min R) . y <= HausDist Q,R by XXREAL_0:2; :: thesis: verum