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