:: deftheorem Def4 defines filled FIN_TOPO:def 4 :
for IT being non empty RelStr holds
( IT is filled iff for x being Element of IT holds x in U_FT x );