for B being B_Lattice
for FB being Filter of B holds
( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )