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 1
.= {0} by Th27 ;
max_dist_min (P,P) = upper_bound ((dist_min P) .: P) by WEIERSTR:def 8
.= upper_bound {0} by A1, WEIERSTR:def 2 ;
hence max_dist_min (P,P) = 0 by SEQ_4:9; :: thesis: verum