theorem Th7: :: JORDAN_A:7

for n being Nat
for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds
dist_min (A,B) > 0