let M be non empty MetrSpace; :: thesis: for P being Subset of (TopSpaceMetr M) st P is compact holds
for p1, p2 being Point of M st p1 in P holds
( dist p1,p2 <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist p1,p2 )
let P be Subset of (TopSpaceMetr M); :: thesis: ( P is compact implies for p1, p2 being Point of M st p1 in P holds
( dist p1,p2 <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist p1,p2 ) )
assume A1: P is compact ; :: thesis: for p1, p2 being Point of M st p1 in P holds
( dist p1,p2 <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist p1,p2 )
let p1, p2 be Point of M; :: thesis: ( p1 in P implies ( dist p1,p2 <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist p1,p2 ) )
assume A2: p1 in P ; :: thesis: ( dist p1,p2 <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist p1,p2 )
dist p2 is continuous by Th22;
then A3: [#] ((dist p2) .: P) is bounded by A1, Th14, Th17;
A4: dist p1,p2 in [#] ((dist p2) .: P)

proof

A5: dist p1,p2 = (dist p2) . p1 by Def6;
dom (dist p2) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
hence dist p1,p2 in [#] ((dist p2) .: P) by A2, A5, FUNCT_1:def 12; :: thesis: verum

end;

A6: dist p1,p2 <= upper_bound ((dist p2) .: P)

proof

[#] ((dist p2) .: P) is bounded_above by A3, XXREAL_2:def 11;
hence dist p1,p2 <= upper_bound ((dist p2) .: P) by A4, SEQ_4:def 4; :: thesis: verum

end;

lower_bound ((dist p2) .: P) <= dist p1,p2

proof

[#] ((dist p2) .: P) is bounded_below by A3, XXREAL_2:def 11;
hence lower_bound ((dist p2) .: P) <= dist p1,p2 by A4, SEQ_4:def 5; :: thesis: verum

end;

hence ( dist p1,p2 <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist p1,p2 ) by A6; :: thesis: verum