let n be Element of NAT ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: P = Q
X: 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)) ;
Y: ( P1 is compact & Q1 is compact ) by A1, X, COMPTS_1:33;
HausDist P1,Q1 = 0 by A2, Def3;
hence P = Q by A1, Th39, Y, X; :: thesis: verum