let M be non empty MetrSpace; :: thesis: for A, B being non empty Subset of (TopSpaceMetr M) holds min_dist_min (A,B) >= 0
let A, B be non empty Subset of (TopSpaceMetr M); :: thesis: min_dist_min (A,B) >= 0
set X = [#] ((dist_min A) .: B);
A1: [#] ((dist_min A) .: B) = (dist_min A) .: B by WEIERSTR:def 1;
A2: for r being Real st r in [#] ((dist_min A) .: B) holds
0 <= r

proof

let r be Real; :: thesis: ( r in [#] ((dist_min A) .: B) implies 0 <= r )
assume r in [#] ((dist_min A) .: B) ; :: thesis: 0 <= r
then consider y being object such that
y in dom (dist_min A) and
A3: y in B and
A4: r = (dist_min A) . y by A1, FUNCT_1:def 6;
reconsider y = y as Point of (TopSpaceMetr M) by A3;
(dist_min A) . y >= 0 by Th9;
hence 0 <= r by A4; :: thesis: verum

end;

dom (dist_min A) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then lower_bound ([#] ((dist_min A) .: B)) >= 0 by A1, A2, SEQ_4:43;
then lower_bound ((dist_min A) .: B) >= 0 by WEIERSTR:def 3;
hence min_dist_min (A,B) >= 0 by WEIERSTR:def 7; :: thesis: verum