theorem :: CARDFIL2:38

for X, Y being non empty set
for f being Function of X,Y
for B1, B2 being filter_base of X st B1 is_coarser_than B2 holds
<.B1.) is_filter-coarser_than <.B2.)