let n be Element of 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:13;
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 A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & dist_min A,B = min_dist_min A',B' ) by Def1;
hence dist_min A,B >= r by A2, Th13; :: thesis: verum