:: deftheorem defines max-ideal FILTER_2:def 8 :
for L being Lattice
for I being Ideal of L holds
( I is max-ideal iff ( I <> the carrier of L & ( for J being Ideal of L st I c= J & J <> the carrier of L holds
I = J ) ) );