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