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_min P) . p1 & x2 = (dist_min P) . p2 holds
abs (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_min P) . p1 & x2 = (dist_min P) . p2 holds
abs (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_min P) . p1 & x2 = (dist_min P) . p2 holds
abs (x1 - x2) <= dist p1,p2
let p1, p2 be Point of M; :: thesis: for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds
abs (x1 - x2) <= dist p1,p2
let x1, x2 be Real; :: thesis: ( x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 implies abs (x1 - x2) <= dist p1,p2 )
assume A2: ( x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 ) ; :: thesis: abs (x1 - x2) <= dist p1,p2
( (dist_min P) . p1 = lower_bound ((dist p1) .: P) & (dist_min P) . p2 = lower_bound ((dist p2) .: P) ) by Def8;
hence abs (x1 - x2) <= dist p1,p2 by A1, A2, Th28; :: thesis: verum