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 holds
HausDist (P,Q) >= 0
let P, Q be non empty Subset of (TOP-REAL n); :: thesis: ( P is compact & Q is compact implies HausDist (P,Q) >= 0 )
A1: 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)) ;
assume ( P is compact & Q is compact ) ; :: thesis: HausDist (P,Q) >= 0
then ( P1 is compact & Q1 is compact ) by A1, COMPTS_1:23;
then HausDist (P1,Q1) >= 0 by Th35;
hence HausDist (P,Q) >= 0 by Def3; :: thesis: verum