:: deftheorem defines Fo_open FINTOPO2:def 16 :
for FMT being non empty FMT_Space_Str
for G being Subset of FMT holds
( G is Fo_open iff G = G ^Foi );