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