let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M) holds max_dist_min P,P = 0
let P be non empty Subset of (TopSpaceMetr M); :: thesis: max_dist_min P,P = 0
A1: [#] ((dist_min P) .: P) = (dist_min P) .: P by WEIERSTR:def 3
.= {0 } by Th29 ;
max_dist_min P,P = upper_bound ((dist_min P) .: P) by WEIERSTR:def 10
.= upper_bound {0 } by A1, WEIERSTR:def 4 ;
hence max_dist_min P,P = 0 by SEQ_4:22; :: thesis: verum