for n being Nat holds TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceNorm (REAL-NS n)