theorem :: FILTER_2:59

for B being B_Lattice
for a, b being Element of B st a <> b holds
ex IB being Ideal of B st
( IB is max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )