let M be non empty MetrSpace; :: thesis: for P being non empty Subset of
for x being Point of holds
( x in Cl P iff (dist_min P) . x = 0 )
let P be non empty Subset of ; :: thesis: for x being Point of holds
( x in Cl P iff (dist_min P) . x = 0 )
let x be Point of ; :: thesis: ( x in Cl P iff (dist_min P) . x = 0 )

hereby :: thesis: ( (dist_min P) . x = 0 implies x in Cl P )

assume x in Cl P ; :: thesis: (dist_min P) . x = 0
then for a being real number st a > 0 holds
ex p being Point of st
( p in P & dist x,p < a ) by Th8;
hence (dist_min P) . x = 0 by Th9; :: thesis: verum

end;

assume (dist_min P) . x = 0 ; :: thesis: x in Cl P
then for a being real number st a > 0 holds
ex p being Point of st
( p in P & dist x,p < a ) by Th9;
hence x in Cl P by Th8; :: thesis: verum