let ET be non empty strict FMT_Space_Str ; :: thesis: ( ET is Fo_filled & ( for x being Element of ET holds not U_FMT x is empty ) implies ET is U_FMT_with_point )
assume that
A1: ET is Fo_filled and
A2: for x being Element of ET holds not U_FMT x is empty ; :: thesis: ET is U_FMT_with_point
for x being Element of ET
for V being Element of U_FMT x holds x in V

proof

let x be Element of ET; :: thesis: for V being Element of U_FMT x holds x in V
let V be Element of U_FMT x; :: thesis: x in V
not U_FMT x is empty by A2;
then V in U_FMT x ;
hence x in V by A1; :: thesis: verum

end;

hence ET is U_FMT_with_point ; :: thesis: verum