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
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P1 = P as non empty Subset of (TopSpaceMetr (Euclid n)) ;
HausDist (P1,P1) = 0 by Th29;
hence HausDist (P,P) = 0 by Def3; :: thesis: verum