let M be non empty MetrSpace; :: thesis: for Q, R being non empty Subset of (TopSpaceMetr M)
for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= max_dist_min R,Q
let Q, R be non empty Subset of (TopSpaceMetr M); :: thesis: for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= max_dist_min R,Q
let y be Point of M; :: thesis: ( Q is compact & R is compact & y in Q implies (dist_min R) . y <= max_dist_min R,Q )
assume that
A1: ( Q is compact & R is compact ) and
A2: y in Q ; :: thesis: (dist_min R) . y <= max_dist_min R,Q
A3: max_dist_min R,Q = upper_bound ((dist_min R) .: Q) by WEIERSTR:def 10;
set A = (dist_min R) .: Q;
consider X being non empty Subset of REAL such that
A4: ( (dist_min R) .: Q = X & upper_bound ((dist_min R) .: Q) = sup X ) by Th13;
A5: X is bounded_above by A1, A4, Th27;
dom (dist_min R) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then (dist_min R) . y in X by A2, A4, FUNCT_1:def 12;
hence (dist_min R) . y <= max_dist_min R,Q by A3, A4, A5, SEQ_4:def 4; :: thesis: verum