let M be non empty MetrSpace; :: thesis: for A, B being compact Subset of (TopSpaceMetr M) st A meets B holds
min_dist_min (A,B) = 0
let A, B be compact Subset of (TopSpaceMetr M); :: thesis: ( A meets B implies min_dist_min (A,B) = 0 )
assume A meets B ; :: thesis: min_dist_min (A,B) = 0
then consider p being object such that
A1: p in A and
A2: p in B by XBOOLE_0:3;
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;
then reconsider p = p as Point of M by A1;
( min_dist_min (A,B) >= 0 & min_dist_min (A,B) <= dist (p,p) ) by A1, A2, Th11, WEIERSTR:34;
hence min_dist_min (A,B) = 0 by METRIC_1:1; :: thesis: verum