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 Th31;
hence HausDist P,P = 0 by Def3; :: thesis: verum