let n be Nat; :: thesis: the carrier of (REAL-NS n) = the carrier of (Euclid n)
thus the carrier of (Euclid n) = the carrier of (TOP-REAL n) by EUCLID:67
.= REAL n by EUCLID:22
.= the carrier of (REAL-NS n) by REAL_NS1:def 4 ; :: thesis: verum