let n be Element of NAT ; :: thesis: for P being non empty Subset of (TOP-REAL n) holds HausDist P,P = 0
let P be non empty Subset of (TOP-REAL n); :: thesis: HausDist P,P = 0
reconsider P1 = P as non empty Subset of (TopSpaceMetr (Euclid n)) ;
HausDist P1,P1 = 0 by Th31;
hence HausDist P,P = 0 by Def3; :: thesis: verum