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