for B being B_Lattice
for a, b being Element of B st a <> b holds
ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )