:: deftheorem defines topological UNIFORM2:def 15 :
for USS being non empty axiom_U1 UniformSpaceStr holds
( USS is topological iff FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #) is FMT_TopSpace );