:: deftheorem Def1 defines open FINTOPO7:def 1 :
for ET being non empty strict FMT_Space_Str
for O being Subset of ET holds
( O is open iff for x being Element of ET st x in O holds
O in U_FMT x );