let n be Nat; :: thesis: for r being Real
for A, B being non empty Subset of (TOP-REAL n) st ( for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ) holds
dist_min (A,B) >= r
let r be Real; :: thesis: for A, B being non empty Subset of (TOP-REAL n) st ( for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ) holds
dist_min (A,B) >= r
let A, B be non empty Subset of (TOP-REAL n); :: thesis: ( ( for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ) implies dist_min (A,B) >= r )
assume A1: for p, q being Point of (TOP-REAL n) st p in A & q in B holds
dist (p,q) >= r ; :: thesis: dist_min (A,B) >= r
A2: for p, q being Point of (Euclid n) st p in A & q in B holds
dist (p,q) >= r

proof

let a, b be Point of (Euclid n); :: thesis: ( a in A & b in B implies dist (a,b) >= r )
assume A3: ( a in A & b in B ) ; :: thesis: dist (a,b) >= r
reconsider p = a, q = b as Point of (TOP-REAL n) by TOPREAL3:8;
ex a, b being Point of (Euclid n) st
( p = a & q = b & dist (p,q) = dist (a,b) ) by TOPREAL6:def 1;
hence dist (a,b) >= r by A1, A3; :: thesis: verum

end;

ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & dist_min (A,B) = min_dist_min (A9,B9) ) by Def1;
hence dist_min (A,B) >= r by A2, Th13; :: thesis: verum