:: deftheorem defines ^Fodel_o FINTOPO2:def 15 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodel_o = (A `) /\ (A ^Fodelta);