:: deftheorem defines FMT_induced_by UNIFORM2:def 19 :
for USS being non empty axiom_U1 topological UniformSpaceStr holds FMT_induced_by USS = FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #);