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

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

hence
ET is U_FMT_with_point
; :: thesis: verum
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;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