let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M)
for x, y being Point of M st y in P & P is compact holds
(dist_max P) . x >= dist (x,y)
let P be non empty Subset of (TopSpaceMetr M); :: thesis: for x, y being Point of M st y in P & P is compact holds
(dist_max P) . x >= dist (x,y)
let x, y be Point of M; :: thesis: ( y in P & P is compact implies (dist_max P) . x >= dist (x,y) )
assume that
A1: y in P and
A2: P is compact ; :: thesis: (dist_max P) . x >= dist (x,y)
consider X being non empty Subset of REAL such that
A3: X = (dist x) .: P and
A4: upper_bound ((dist x) .: P) = upper_bound X by Th11;
A5: (dist_max P) . x = upper_bound X by A4, WEIERSTR:def 5;
( dom (dist x) = the carrier of (TopSpaceMetr M) & dist (x,y) = (dist x) . y ) by FUNCT_2:def 1, WEIERSTR:def 4;
then A6: dist (x,y) in X by A1, A3, FUNCT_1:def 6;
X is bounded_above by A2, A3, Lm1;
hence (dist_max P) . x >= dist (x,y) by A5, A6, SEQ_4:def 1; :: thesis: verum