let ET be non empty strict FMT_Space_Str ; :: thesis: ( ET is Fo_filled & ET is U_FMT_filter implies ET is U_FMT_with_point )
assume that
A1: ET is Fo_filled and
A2: ET is U_FMT_filter ; :: thesis: ET is U_FMT_with_point
for x being Element of ET holds not U_FMT x is empty by A2;
hence ET is U_FMT_with_point by A1, Th5; :: thesis: verum