theorem :: FILTER_2:56

for B being B_Lattice
for IB being Ideal of B holds
( IB is max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )