:: deftheorem Def4 defines U_FMT_local FINTOPO7:def 4 :
for ET being non empty strict FMT_Space_Str holds
( ET is U_FMT_local iff for x being Element of ET
for V being Element of U_FMT x ex W being Element of U_FMT x st
for y being Element of ET st y is Element of W holds
V is Element of U_FMT y );