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 that

A1: P <> {} and

A2: P is compact and

A3: Q <> {} and

A4: Q is compact ; :: thesis: ( P misses Q iff min_dist_min (P,Q) > 0 )

A9: ( x1 in P & x2 in Q ) and

A10: dist (x1,x2) = min_dist_min (P,Q) by A1, A2, A3, A4, WEIERSTR:30;

A11: the distance of M is discerning by METRIC_1:def 7;

( 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 that

A1: P <> {} and

A2: P is compact and

A3: Q <> {} and

A4: Q is compact ; :: thesis: ( P misses Q iff min_dist_min (P,Q) > 0 )

A5: now :: thesis: ( P /\ Q <> {} implies not min_dist_min (P,Q) > 0 )

consider x1, x2 being Point of M such that set p = the Element of P /\ Q;

assume A6: P /\ Q <> {} ; :: thesis: not min_dist_min (P,Q) > 0

then A7: the Element of P /\ Q in P by XBOOLE_0:def 4;

then reconsider p9 = the Element of P /\ Q as Element of (TopSpaceMetr M) ;

reconsider q = p9 as Point of M by TOPMETR:12;

the distance of M is Reflexive by METRIC_1:def 6;

then the distance of M . (q,q) = 0 by METRIC_1:def 2;

then A8: dist (q,q) = 0 by METRIC_1:def 1;

the Element of P /\ Q in Q by A6, XBOOLE_0:def 4;

hence not min_dist_min (P,Q) > 0 by A2, A4, A7, A8, WEIERSTR:34; :: thesis: verum

end;assume A6: P /\ Q <> {} ; :: thesis: not min_dist_min (P,Q) > 0

then A7: the Element of P /\ Q in P by XBOOLE_0:def 4;

then reconsider p9 = the Element of P /\ Q as Element of (TopSpaceMetr M) ;

reconsider q = p9 as Point of M by TOPMETR:12;

the distance of M is Reflexive by METRIC_1:def 6;

then the distance of M . (q,q) = 0 by METRIC_1:def 2;

then A8: dist (q,q) = 0 by METRIC_1:def 1;

the Element of P /\ Q in Q by A6, XBOOLE_0:def 4;

hence not min_dist_min (P,Q) > 0 by A2, A4, A7, A8, WEIERSTR:34; :: thesis: verum

A9: ( x1 in P & x2 in Q ) and

A10: dist (x1,x2) = min_dist_min (P,Q) by A1, A2, A3, A4, WEIERSTR:30;

A11: the distance of M is discerning by METRIC_1:def 7;

now :: thesis: ( not min_dist_min (P,Q) > 0 implies P /\ Q <> {} )

hence
( P misses Q iff min_dist_min (P,Q) > 0 )
by A5; :: thesis: verumassume
not min_dist_min (P,Q) > 0
; :: thesis: P /\ Q <> {}

then dist (x1,x2) = 0 by A1, A2, A3, A4, A10, Th36;

then the distance of M . (x1,x2) = 0 by METRIC_1:def 1;

then x1 = x2 by A11, METRIC_1:def 3;

hence P /\ Q <> {} by A9, XBOOLE_0:def 4; :: thesis: verum

end;then dist (x1,x2) = 0 by A1, A2, A3, A4, A10, Th36;

then the distance of M . (x1,x2) = 0 by METRIC_1:def 1;

then x1 = x2 by A11, METRIC_1:def 3;

hence P /\ Q <> {} by A9, XBOOLE_0:def 4; :: thesis: verum