:: deftheorem defines U_FMT_filter_base FINTOPO7:def 8 :
for ET being non empty strict FMT_Space_Str holds
( ET is U_FMT_filter_base iff for x being Element of the carrier of ET holds U_FMT x is filter_base of the carrier of ET );