theorem :: CARDFIL2:36

for X being non empty set
for B being filter_base of X st B = <.B.) holds
B is Filter of X ;