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 Th21;
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:40;
hence (dist_min P) . z <= max_dist_max P,Q by A2, XXREAL_0:2; :: thesis: verum