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