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