:: deftheorem defines Fo_filled FINTOPO2:def 8 :
for IT being non empty FMT_Space_Str holds
( IT is Fo_filled iff for x being Element of IT
for D being Subset of IT st D in U_FMT x holds
x in D );