:: deftheorem defines ^Fon FINTOPO2:def 13 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fon = A \ (A ^Fos);