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_max 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_max 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_max P) . z <= max_dist_max P,Q )
assume A1: ( P is compact & Q is compact ) ; :: thesis: ( not z in Q or (dist_max P) . z <= max_dist_max P,Q )
then reconsider P = P as non empty compact Subset of (TopSpaceMetr M) ;
assume A2: z in Q ; :: thesis: (dist_max P) . z <= max_dist_max P,Q
A3: upper_bound ((dist_max P) .: Q) = max_dist_max P,Q by WEIERSTR:def 12;
set A = (dist_max P) .: Q;
consider X being non empty Subset of REAL such that
A4: ( (dist_max P) .: Q = X & max_dist_max P,Q = sup X ) by A3, Th13;
[#] ((dist_max P) .: Q) is bounded by A1, WEIERSTR:15, WEIERSTR:17;
then X is bounded by A4, WEIERSTR:def 3;
then A5: X is bounded_above by XXREAL_2:def 11;
dom (dist_max P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then (dist_max P) . z in (dist_max P) .: Q by A2, FUNCT_1:def 12;
hence (dist_max P) . z <= max_dist_max P,Q by A4, A5, SEQ_4:def 4; :: thesis: verum