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 )
assume A1: ( P is compact & Q is compact ) ; :: thesis: HausDist P,Q >= 0
reconsider P1 = P, Q1 = Q as non empty Subset of (TopSpaceMetr (Euclid n)) ;
HausDist P1,Q1 >= 0 by A1, Th37;
hence HausDist P,Q >= 0 by Def3; :: thesis: verum