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 )
assume that
A1: ( P is compact & Q is compact ) and
A2: z in Q ; :: thesis: (dist_min P) . z <= max_dist_max P,Q
consider w being Point of M such that
A3: ( w in P & (dist_min P) . z <= dist w,z ) by Th21;
dist w,z <= max_dist_max P,Q by A1, A2, A3, WEIERSTR:40;
hence (dist_min P) . z <= max_dist_max P,Q by A3, XXREAL_0:2; :: thesis: verum