let n be Nat; :: thesis: [#] (TOP-REAL n) = [#] (Euclid n)
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
hence [#] (TOP-REAL n) = [#] (Euclid n) ; :: thesis: verum