:: deftheorem defines ^Foi FINTOPO2:def 11 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Foi = { x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A ) } ;