for B being B_Lattice
for IB being Ideal of B st IB is max-ideal holds
for a being Element of B holds
( a in IB iff not a ` in IB )