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 Th16;
then [#] ((dist p2) .: P) is real-bounded by A1, Th8, Th11;
then A2: ( [#] ((dist p2) .: P) is bounded_above & [#] ((dist p2) .: P) is bounded_below ) ;
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 Def4, FUNCT_2:def 1;
then dist (p1,p2) in [#] ((dist p2) .: P) by A3, FUNCT_1:def 6;
hence ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) by A2, SEQ_4:def 1, SEQ_4:def 2; :: thesis: verum