ex US being strict UniformSpace st US = uniformity_induced_by MS by Th10;
hence UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #) is non empty strict UniformSpace ; :: thesis: verum