theorem Th39: :: EUCLID:67

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