:: deftheorem defines uniformity_induced_by UNIFORM3:def 4 :
for MS being non empty MetrStruct holds uniformity_induced_by MS = UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #);