theorem Th10: :: COUSIN:13

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