let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M) holds (dist_min P) .: P = {0 }
let P be non empty Subset of (TopSpaceMetr M); :: thesis: (dist_min P) .: P = {0 }
thus (dist_min P) .: P c= {0 } :: according to XBOOLE_0:def 10 :: thesis: {0 } c= (dist_min P) .: P

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (dist_min P) .: P or y in {0 } )
assume y in (dist_min P) .: P ; :: thesis: y in {0 }
then consider x being set such that
x in dom (dist_min P) and
A1: x in P and
A2: y = (dist_min P) . x by FUNCT_1:def 12;
y = 0 by A1, A2, Th5;
hence y in {0 } by TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {0 } or y in (dist_min P) .: P )
assume y in {0 } ; :: thesis: y in (dist_min P) .: P
then A3: y = 0 by TARSKI:def 1;
consider x being set such that
A4: x in P by XBOOLE_0:def 1;
A5: y = (dist_min P) . x by A3, A4, Th5;
dom (dist_min P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
hence y in (dist_min P) .: P by A4, A5, FUNCT_1:def 12; :: thesis: verum