let n be Nat; :: thesis: the carrier of (Euclid n) = the carrier of (TOP-REAL n)
thus the carrier of (Euclid n) = the carrier of (TopSpaceMetr (Euclid n))
.= the carrier of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by Def8
.= the carrier of (TOP-REAL n) ; :: thesis: verum