for X being non empty set
for F being Filter of X
for B being non empty Subset of F holds
( F is_coarser_than B iff B is filter_basis )