theorem :: CARDFIL2:27

for X being non empty set
for FB being filter_base of X
for F being Filter of X st FB c= F holds
<.FB.) is_coarser_than F