let n be Nat; :: thesis: [#] (TOP-REAL n) = [#] (TopSpaceMetr (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) = [#] (TopSpaceMetr (Euclid n)) ; :: thesis: verum