:: deftheorem defines # CARDFIL2:def 10 :
for X being non empty set
for F being Filter of X
for B being non empty Subset of F holds # B = B;