TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
hence 0* n is Point of (TOP-REAL n) ; :: thesis: verum