theorem Th5: :: FINTOPO7:8

for ET being non empty strict FMT_Space_Str st ET is Fo_filled & ( for x being Element of ET holds not U_FMT x is empty ) holds
ET is U_FMT_with_point