:: deftheorem defines Filt CARDFIL2:def 3 :
for X being non empty set holds Filt X = { F where F is Filter of X : verum } ;