let n be Element of NAT ; for A, B being non empty compact Subset of st A misses B holds
dist_min A,B > 0
let A, B be non empty compact Subset of ; ( A misses B implies dist_min A,B > 0 )
assume A1:
A misses B
; 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 A', B' being Subset of such that
A3:
A = A'
and
A4:
B = B'
and
A5:
dist_min A,B = min_dist_min A',B'
by JORDAN1K:def 1;
A6:
A' is compact
by A2, A3, COMPTS_1:33;
B' is compact
by A2, A4, COMPTS_1:33;
hence
dist_min A,B > 0
by A1, A3, A4, A5, A6, JGRAPH_1:55; verum