let M be non empty MetrSpace; :: thesis: for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & HausDist P,Q = 0 holds
P = Q
let P, Q be non empty Subset of (TopSpaceMetr M); :: thesis: ( P is compact & Q is compact & HausDist P,Q = 0 implies P = Q )
assume A1: ( P is compact & Q is compact ) ; :: thesis: ( not HausDist P,Q = 0 or P = Q )
then A2: ( P is closed & Q is closed ) by COMPTS_1:16;
A3: ( max_dist_min P,Q >= 0 & max_dist_min Q,P >= 0 ) by A1, Th30;
assume HausDist P,Q = 0 ; :: thesis: P = Q
then ( max_dist_min P,Q = 0 & max_dist_min Q,P = 0 ) by A3, Th1;
then A4: ( upper_bound ((dist_min P) .: Q) = 0 & upper_bound ((dist_min Q) .: P) = 0 ) by WEIERSTR:def 10;
then consider X being non empty Subset of REAL such that
A5: ( (dist_min P) .: Q = X & 0 = sup X ) by Th13;
consider Y being non empty Subset of REAL such that
A6: ( (dist_min Q) .: P = Y & 0 = sup Y ) by A4, Th13;
A7: Y is bounded_above by A1, A6, Th27;
A8: X is bounded_above by A1, A5, Th27;
thus P c= Q :: according to XBOOLE_0:def 10 :: thesis: Q c= P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in Q )
assume A9: x in P ; :: thesis: x in Q
then reconsider x' = x as Point of M by TOPMETR:16;
dom (dist_min Q) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then (dist_min Q) . x in Y by A6, A9, FUNCT_1:def 12;
then A10: (dist_min Q) . x <= 0 by A6, A7, SEQ_4:def 4;
(dist_min Q) . x >= 0 by A9, JORDAN1K:9;
then (dist_min Q) . x = 0 by A10, XXREAL_0:1;
then x' in Q by A2, Th11;
hence x in Q ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in P )
assume A11: x in Q ; :: thesis: x in P
then reconsider x' = x as Point of M by TOPMETR:16;
dom (dist_min P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then (dist_min P) . x in X by A5, A11, FUNCT_1:def 12;
then A12: (dist_min P) . x <= 0 by A5, A8, SEQ_4:def 4;
(dist_min P) . x >= 0 by A11, JORDAN1K:9;
then (dist_min P) . x = 0 by A12, XXREAL_0:1;
then x' in P by A2, Th11;
hence x in P ; :: thesis: verum