let M be non empty MetrSpace; :: thesis: for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds
|.(x1 - x2).| <= dist (p1,p2)
let P be Subset of (TopSpaceMetr M); :: thesis: ( P <> {} & P is compact implies for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds
|.(x1 - x2).| <= dist (p1,p2) )
assume A1: ( P <> {} & P is compact ) ; :: thesis: for p1, p2 being Point of M
for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds
|.(x1 - x2).| <= dist (p1,p2)
let p1, p2 be Point of M; :: thesis: for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds
|.(x1 - x2).| <= dist (p1,p2)
let x1, x2 be Real; :: thesis: ( x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 implies |.(x1 - x2).| <= dist (p1,p2) )
assume A2: ( x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 ) ; :: thesis: |.(x1 - x2).| <= dist (p1,p2)
( (dist_max P) . p1 = upper_bound ((dist p1) .: P) & (dist_max P) . p2 = upper_bound ((dist p2) .: P) ) by Def5;
hence |.(x1 - x2).| <= dist (p1,p2) by A1, A2, Th20; :: thesis: verum