:: deftheorem defines maximal LATTICEA:def 4 :
for L being Lattice
for I being Ideal of L holds
( I is maximal iff ( I is proper & ( for J being Ideal of L st J is proper & I c= J holds
I = J ) ) );