for B being B_Lattice
for FB being Filter of B st FB is being_ultrafilter holds
for a being Element of B holds
( a in FB iff not a ` in FB )