:: deftheorem defines TopSpace_induced_by UNIFORM2:def 20 :
for USS being non empty axiom_U1 topological UniformSpaceStr holds TopSpace_induced_by USS = FMT2TopSpace (FMT_induced_by USS);