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