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

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