let M be non empty MetrSpace; :: thesis: for P, Q being non empty Subset of (TopSpaceMetr M)
for z being Point of M st P is compact & Q is compact & z in Q holds
(dist_min P) . z <= max_dist_max (P,Q)
let P, Q be non empty Subset of (TopSpaceMetr M); :: thesis: for z being Point of M st P is compact & Q is compact & z in Q holds
(dist_min P) . z <= max_dist_max (P,Q)
let z be Point of M; :: thesis: ( P is compact & Q is compact & z in Q implies (dist_min P) . z <= max_dist_max (P,Q) )
consider w being Point of M such that
A1: w in P and
A2: (dist_min P) . z <= dist (w,z) by Th19;
assume ( P is compact & Q is compact & z in Q ) ; :: thesis: (dist_min P) . z <= max_dist_max (P,Q)
then dist (w,z) <= max_dist_max (P,Q) by A1, WEIERSTR:34;
hence (dist_min P) . z <= max_dist_max (P,Q) by A2, XXREAL_0:2; :: thesis: verum