theorem Th11: :: CARDFIL2:33

for X being non empty set
for F1, F2 being Filter of X
for B1 being basis of F1
for B2 being basis of F2 holds
( F1 is_filter-coarser_than F2 iff B1 is_coarser_than B2 )