let n be 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
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that
A3: A = A9 and
A4: B = B9 and
A5: dist_min (A,B) = min_dist_min (A9,B9) by JORDAN1K:def 1;
A6: A9 is compact by A2, A3, COMPTS_1:23;
B9 is compact by A2, A4, COMPTS_1:23;
hence dist_min (A,B) > 0 by A1, A3, A4, A5, A6, JGRAPH_1:38; :: thesis: verum