let M be non empty MetrSpace; 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); ( 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
; 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; ( 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
; ( 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; verum