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}
consider x being object such that
A1: x in P by XBOOLE_0:def 1;
thus (dist_min P) .: P c= {0} :: according to XBOOLE_0:def 10 :: thesis: {0} c= (dist_min P) .: P
proof
let y be object ; :: 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 ex x being object st
( x in dom (dist_min P) & x in P & y = (dist_min P) . x ) by FUNCT_1:def 6;
then y = 0 by Th5;
hence y in {0} by TARSKI:def 1; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {0} or y in (dist_min P) .: P )
A2: dom (dist_min P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
assume y in {0} ; :: thesis: y in (dist_min P) .: P
then y = 0 by TARSKI:def 1;
then y = (dist_min P) . x by A1, Th5;
hence y in (dist_min P) .: P by A1, A2, FUNCT_1:def 6; :: thesis: verum