:: deftheorem defines Extend_Filter CARD_FIL:def 8 :
for X being non empty set
for F being Filter of X
for Z being Subset of X holds Extend_Filter (F,Z) = { Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } ;