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