theorem Th4: :: REAL_NS2:4

for n being Nat holds the carrier of (TOP-REAL n) = the carrier of (REAL-NS n)