:: deftheorem def2 defines filter_basis CARDFIL2:def 7 :
for X being non empty set
for F being Filter of X
for B being non empty Subset of F holds
( B is filter_basis iff for f being Element of F ex b being Element of B st b c= f );