let n be Element of NAT ; :: thesis: for A, B being compact Subset of (TOP-REAL n) st A meets B holds
dist_min A,B = 0
let A, B be compact Subset of (TOP-REAL n); :: thesis: ( A meets B implies dist_min A,B = 0 )
assume A1: A meets B ; :: thesis: dist_min A,B = 0
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 = 0 by A1, Th12; :: thesis: verum