theorem Th8: :: FINTOPO7:13

for ET being non empty strict FMT_Space_Str st ET is U_FMT_filter_base holds
gen_filter ET is U_FMT_filter