:: deftheorem defines is_filter-coarser_than CARDFIL2:def 5 :
for X being non empty set
for F1, F2 being Filter of X holds
( F1 is_filter-coarser_than F2 iff F1 c= F2 );