let M be non empty MetrSpace; 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); 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; ( P is compact & Q is compact & z in Q implies (dist_max P) . z <= max_dist_max (P,Q) )
assume that
A1:
P is compact
and
A2:
Q is compact
; ( not z in Q or (dist_max P) . z <= max_dist_max (P,Q) )
reconsider P = P as non empty compact Subset of (TopSpaceMetr M) by A1;
set A = (dist_max P) .: Q;
A3:
dom (dist_max P) = the carrier of (TopSpaceMetr M)
by FUNCT_2:def 1;
assume
z in Q
; (dist_max P) . z <= max_dist_max (P,Q)
then A4:
(dist_max P) . z in (dist_max P) .: Q
by A3, FUNCT_1:def 6;
upper_bound ((dist_max P) .: Q) = max_dist_max (P,Q)
by WEIERSTR:def 10;
then consider X being non empty Subset of REAL such that
A5:
(dist_max P) .: Q = X
and
A6:
max_dist_max (P,Q) = upper_bound X
by Th11;
[#] ((dist_max P) .: Q) is real-bounded
by A2, WEIERSTR:9, WEIERSTR:11;
then
X is real-bounded
by A5, WEIERSTR:def 1;
then
X is bounded_above
;
hence
(dist_max P) . z <= max_dist_max (P,Q)
by A5, A6, A4, SEQ_4:def 1; verum