let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M)
for x being Point of M holds
( x in Cl P iff (dist_min P) . x = 0 )
let P be non empty Subset of (TopSpaceMetr M); :: thesis: for x being Point of M holds
( x in Cl P iff (dist_min P) . x = 0 )
let x be Point of M; :: 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 st a > 0 holds
ex p being Point of M st
( p in P & dist (x,p) < a ) by Th6;
hence (dist_min P) . x = 0 by Th7; :: thesis: verum
end;
assume (dist_min P) . x = 0 ; :: thesis: x in Cl P
then for a being Real st a > 0 holds
ex p being Point of M st
( p in P & dist (x,p) < a ) by Th7;
hence x in Cl P by Th6; :: thesis: verum