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