let M be non empty MetrSpace; :: thesis: for P, Q being Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min P,Q <= dist x1,x2 & dist x1,x2 <= max_dist_max P,Q )
let P, Q be Subset of (TopSpaceMetr M); :: thesis: ( P is compact & Q is compact implies for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min P,Q <= dist x1,x2 & dist x1,x2 <= max_dist_max P,Q ) )
assume A1: ( P is compact & Q is compact ) ; :: thesis: for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min P,Q <= dist x1,x2 & dist x1,x2 <= max_dist_max P,Q )
let x1, x2 be Point of M; :: thesis: ( x1 in P & x2 in Q implies ( min_dist_min P,Q <= dist x1,x2 & dist x1,x2 <= max_dist_max P,Q ) )
assume A2: ( x1 in P & x2 in Q ) ; :: thesis: ( min_dist_min P,Q <= dist x1,x2 & dist x1,x2 <= max_dist_max P,Q )
A3: dom (dist_max P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
x2 in the carrier of M ;
then x2 in the carrier of (TopSpaceMetr M) by TOPMETR:16;
then (dist_max P) . x2 in the carrier of R^1 by FUNCT_2:7;
then consider y being Real such that
A4: y = (dist_max P) . x2 by TOPMETR:24;
A5: upper_bound ((dist x2) .: P) = y by A4, Def7;
dist_max P is continuous by A1, A2, Th30;
then A6: [#] ((dist_max P) .: Q) is bounded by A1, Th14, Th17;
A7: y in [#] ((dist_max P) .: Q) by A2, A3, A4, FUNCT_1:def 12;
A8: y <= upper_bound ((dist_max P) .: Q)

proof

[#] ((dist_max P) .: Q) is bounded_above by A6, XXREAL_2:def 11;
hence y <= upper_bound ((dist_max P) .: Q) by A7, SEQ_4:def 4; :: thesis: verum

end;

A9: dom (dist_min P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
x2 in the carrier of M ;
then x2 in the carrier of (TopSpaceMetr M) by TOPMETR:16;
then (dist_min P) . x2 in the carrier of R^1 by FUNCT_2:7;
then consider z being Real such that
A10: z = (dist_min P) . x2 by TOPMETR:24;
A11: ( dist x1,x2 <= upper_bound ((dist x2) .: P) & lower_bound ((dist x2) .: P) <= dist x1,x2 ) by A1, A2, Th25;
A12: lower_bound ((dist x2) .: P) = z by A10, Def8;
dist_min P is continuous by A1, A2, Th33;
then A13: [#] ((dist_min P) .: Q) is bounded by A1, Th14, Th17;
A14: z in [#] ((dist_min P) .: Q) by A2, A9, A10, FUNCT_1:def 12;
lower_bound ((dist_min P) .: Q) <= z

proof

[#] ((dist_min P) .: Q) is bounded_below by A13, XXREAL_2:def 11;
hence lower_bound ((dist_min P) .: Q) <= z by A14, SEQ_4:def 5; :: thesis: verum

end;

hence ( min_dist_min P,Q <= dist x1,x2 & dist x1,x2 <= max_dist_max P,Q ) by A5, A8, A11, A12, XXREAL_0:2; :: thesis: verum