:: deftheorem Def1 defines Filter CARD_FIL:def 1 :
for X being non empty set
for b₂ being non empty Subset-Family of X holds
( b₂ is Filter of X iff ( not {} in b₂ & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b₂ & Y2 in b₂ implies Y1 /\ Y2 in b₂ ) & ( Y1 in b₂ & Y1 c= Y2 implies Y2 in b₂ ) ) ) ) );