theorem Th4: :: FINTOPO7:6

for ET being non empty strict FMT_Space_Str st ET is U_FMT_filter holds
for x being Element of ET holds not U_FMT x is empty ;