theorem Th8: :: TOPREAL3:8

for n being Nat holds the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:22;