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 ) )
dist p2 is continuous by Th22;
then [#] ((dist p2) .: P) is bounded by A1, Th14, Th17;
then A2: ( [#] ((dist p2) .: P) is bounded_above & [#] ((dist p2) .: P) is bounded_below ) by XXREAL_2:def 11;
assume A3: p1 in P ; :: thesis: ( dist p1,p2 <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist p1,p2 )
( dist p1,p2 = (dist p2) . p1 & dom (dist p2) = the carrier of (TopSpaceMetr M) ) by Def6, FUNCT_2:def 1;
then dist p1,p2 in [#] ((dist p2) .: P) by A3, FUNCT_1:def 12;
hence ( dist p1,p2 <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist p1,p2 ) by A2, SEQ_4:def 4, SEQ_4:def 5; :: thesis: verum