for UT being non empty strict Quasi-UniformSpace
for FMT being non empty strict FMT_Space_Str
for x being Element of FMT st FMT = FMT_Space_Str(# the carrier of UT,(Neighborhood UT) #) holds
ex y being Element of UT st
( x = y & U_FMT x = Neighborhood y )