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 that
A1: P is compact and
A2: Q is compact ; :: thesis: ( not HausDist (P,Q) = 0 or P = Q )
A3: Q is closed by A2, COMPTS_1:7;
assume A4: HausDist (P,Q) = 0 ; :: thesis: P = Q
then max_dist_min (Q,P) = 0 by A1, A2, Th1, Th28;
then upper_bound ((dist_min Q) .: P) = 0 by WEIERSTR:def 8;
then consider Y being non empty Subset of REAL such that
A5: (dist_min Q) .: P = Y and
A6: 0 = upper_bound Y by Th11;
A7: Y is bounded_above by A1, A2, A5, Th25;
thus P c= Q :: according to XBOOLE_0:def 10 :: thesis: Q c= P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in Q )
assume A8: x in P ; :: thesis: x in Q
then reconsider x9 = x as Point of M by TOPMETR:12;
dom (dist_min Q) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then (dist_min Q) . x in Y by A5, A8, FUNCT_1:def 6;
then A9: (dist_min Q) . x <= 0 by A6, A7, SEQ_4:def 1;
(dist_min Q) . x >= 0 by A8, JORDAN1K:9;
then (dist_min Q) . x = 0 by A9, XXREAL_0:1;
then x9 in Q by A3, Th9;
hence x in Q ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in P )
assume A10: x in Q ; :: thesis: x in P
then reconsider x9 = x as Point of M by TOPMETR:12;
A11: P is closed by A1, COMPTS_1:7;
max_dist_min (P,Q) = 0 by A1, A2, A4, Th1, Th28;
then upper_bound ((dist_min P) .: Q) = 0 by WEIERSTR:def 8;
then consider X being non empty Subset of REAL such that
A12: (dist_min P) .: Q = X and
A13: 0 = upper_bound X by Th11;
dom (dist_min P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then A14: (dist_min P) . x in X by A12, A10, FUNCT_1:def 6;
X is bounded_above by A1, A2, A12, Th25;
then A15: (dist_min P) . x <= 0 by A13, A14, SEQ_4:def 1;
(dist_min P) . x >= 0 by A10, JORDAN1K:9;
then (dist_min P) . x = 0 by A15, XXREAL_0:1;
then x9 in P by A11, Th9;
hence x in P ; :: thesis: verum