:: deftheorem defines Filters CARD_FIL:def 9 :
for X being non empty set holds Filters X = { S where S is Subset-Family of X : S is Filter of X } ;