:: deftheorem defines U_FMT FINTOPO2:def 6 :
for FMT being non empty FMT_Space_Str
for x being Element of FMT holds U_FMT x = the BNbd of FMT . x;