let M be non empty MetrSpace; :: thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
( P misses Q iff min_dist_min P,Q > 0 )
let P, Q be Subset of (TopSpaceMetr M); :: thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ( P misses Q iff min_dist_min P,Q > 0 ) )
assume A1: ( P <> {} & P is compact & Q <> {} & Q is compact ) ; :: thesis: ( P misses Q iff min_dist_min P,Q > 0 )
then consider x1, x2 being Point of M such that
A2: ( x1 in P & x2 in Q & dist x1,x2 = min_dist_min P,Q ) by WEIERSTR:36;
A3: the distance of M is discerning by METRIC_1:def 8;

A4: now

assume not min_dist_min P,Q > 0 ; :: thesis: P /\ Q <> {}
then dist x1,x2 = 0 by A1, A2, Th54;
then the distance of M . x1,x2 = 0 by METRIC_1:def 1;
then x1 = x2 by A3, METRIC_1:def 4;
hence P /\ Q <> {} by A2, XBOOLE_0:def 4; :: thesis: verum

end;

now

assume A5: P /\ Q <> {} ; :: thesis: not min_dist_min P,Q > 0
consider p being Element of P /\ Q;
A6: ( p in P & p in Q ) by A5, XBOOLE_0:def 4;
then reconsider p' = p as Element of (TopSpaceMetr M) ;
reconsider q = p' as Point of M by TOPMETR:16;
the distance of M is Reflexive by METRIC_1:def 7;
then the distance of M . q,q = 0 by METRIC_1:def 3;
then dist q,q = 0 by METRIC_1:def 1;
hence not min_dist_min P,Q > 0 by A1, A6, WEIERSTR:40; :: thesis: verum

end;

hence ( P misses Q iff min_dist_min P,Q > 0 ) by A4, XBOOLE_0:def 7; :: thesis: verum