let r be Real; :: thesis: for M being non empty MetrSpace
for A, B being non empty Subset of (TopSpaceMetr M) st ( for p, q being Point of M st p in A & q in B holds
dist p,q >= r ) holds
min_dist_min A,B >= r
let M be non empty MetrSpace; :: thesis: for A, B being non empty Subset of (TopSpaceMetr M) st ( for p, q being Point of M st p in A & q in B holds
dist p,q >= r ) holds
min_dist_min A,B >= r
let A, B be non empty Subset of (TopSpaceMetr M); :: thesis: ( ( for p, q being Point of M st p in A & q in B holds
dist p,q >= r ) implies min_dist_min A,B >= r )
assume A1: for p, q being Point of M st p in A & q in B holds
dist p,q >= r ; :: thesis: min_dist_min A,B >= r
set X = [#] ((dist_min A) .: B);
A2: [#] ((dist_min A) .: B) = (dist_min A) .: B by WEIERSTR:def 3;
A3: for s being real number st s in [#] ((dist_min A) .: B) holds
r <= s

proof

let s be real number ; :: thesis: ( s in [#] ((dist_min A) .: B) implies r <= s )
assume s in [#] ((dist_min A) .: B) ; :: thesis: r <= s
then consider y being set such that
y in dom (dist_min A) and
A4: y in B and
A5: s = (dist_min A) . y by A2, FUNCT_1:def 12;
reconsider y = y as Point of (TopSpaceMetr M) by A4;
reconsider p = y as Point of M by TOPMETR:16;
for q being Point of M st q in A holds
dist p,q >= r by A1, A4;
hence r <= s by A5, Th10; :: thesis: verum

end;

dom (dist_min A) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then lower_bound ([#] ((dist_min A) .: B)) >= r by A3, A2, SEQ_4:60;
then lower_bound ((dist_min A) .: B) >= r by WEIERSTR:def 5;
hence min_dist_min A,B >= r by WEIERSTR:def 9; :: thesis: verum