for X being non empty set
for F, FX being Filter of X st FX = {X} holds
FX is_coarser_than F