theorem Th19: :: EUCLID:22

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