let M be non empty MetrSpace; :: thesis: for P being non empty closed Subset of (TopSpaceMetr M)
for x being Point of M holds
( x in P iff (dist_min P) . x = 0 )
let P be non empty closed Subset of (TopSpaceMetr M); :: thesis: for x being Point of M holds
( x in P iff (dist_min P) . x = 0 )
let x be Point of M; :: thesis: ( x in P iff (dist_min P) . x = 0 )
P = Cl P by PRE_TOPC:22;
hence ( x in P iff (dist_min P) . x = 0 ) by Th8; :: thesis: verum