let n be Element of NAT ; :: thesis: for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds
dist_min A,B > 0
let A, B be non empty compact Subset of (TOP-REAL n); :: thesis: ( A misses B implies dist_min A,B > 0 )
assume A1: A misses B ; :: thesis: dist_min A,B > 0
X: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
consider A', B' being Subset of (TopSpaceMetr (Euclid n)) such that
A2: ( A = A' & B = B' ) and
A3: dist_min A,B = min_dist_min A',B' by JORDAN1K:def 1;
( A' is compact & B' is compact ) by X, COMPTS_1:33, A2;
hence dist_min A,B > 0 by A1, A2, A3, JGRAPH_1:55; :: thesis: verum