theorem :: FINTOPO7:7
for ET being non empty strict FMT_Space_Str st ET is U_FMT_with_point holds
ET is Fo_filled ;