:: deftheorem Def2 defines U_FMT_filter FINTOPO7:def 2 :
for ET being non empty strict FMT_Space_Str holds
( ET is U_FMT_filter iff for x being Element of ET holds U_FMT x is Filter of the carrier of ET );