:: deftheorem Def3 defines U_FMT_with_point FINTOPO7:def 3 :
for ET being non empty strict FMT_Space_Str holds
( ET is U_FMT_with_point iff for x being Element of ET
for V being Element of U_FMT x holds x in V );