let n be Nat; :: thesis: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceNorm (REAL-NS n)
thus TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8
.= TopSpaceNorm (REAL-NS n) by Th2 ; :: thesis: verum