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 set 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 6;
then reconsider p = p as Point of M by A1;
A3: min_dist_min A,B >= 0 by A1, A2, Th11;
min_dist_min A,B <= dist p,p by A1, A2, WEIERSTR:40;
hence min_dist_min A,B = 0 by A3, METRIC_1:1; :: thesis: verum