let n be Element of NAT ; for P, Q being non empty Subset of (TOP-REAL n) st P is compact & Q is compact & HausDist (P,Q) = 0 holds
P = Q
let P, Q be non empty Subset of (TOP-REAL n); ( P is compact & Q is compact & HausDist (P,Q) = 0 implies P = Q )
assume that
A1:
( P is compact & Q is compact )
and
A2:
HausDist (P,Q) = 0
; P = Q
A3:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider P1 = P, Q1 = Q as non empty Subset of (TopSpaceMetr (Euclid n)) ;
A4:
HausDist (P1,Q1) = 0
by A2, Def3;
( P1 is compact & Q1 is compact )
by A1, A3, COMPTS_1:23;
hence
P = Q
by A4, Th37; verum