let L be Lattice; :: thesis: for I being Ideal of L holds
( I is max-ideal iff I is maximal )
let I be Ideal of L; :: thesis: ( I is max-ideal iff I is maximal )

hereby :: thesis: ( I is maximal implies I is max-ideal )

assume A0: I is max-ideal ; :: thesis: I is maximal
then a2: I <> the carrier of L by FILTER_2:def 8;
for G being Ideal of L st G is proper & I c= G holds
I = G

proof

let G be Ideal of L; :: thesis: ( G is proper & I c= G implies I = G )
assume B1: ( G is proper & I c= G ) ; :: thesis: I = G
then G <> the carrier of L by SUBSET_1:def 6;
hence I = G by FILTER_2:def 8, A0, B1; :: thesis: verum

end;

hence I is maximal by a2, SUBSET_1:def 6; :: thesis: verum

end;

assume A0: I is maximal ; :: thesis: I is max-ideal
for J being Ideal of L st I c= J & J <> the carrier of L holds
I = J

proof

let J be Ideal of L; :: thesis: ( I c= J & J <> the carrier of L implies I = J )
assume B1: ( I c= J & J <> the carrier of L ) ; :: thesis: I = J
then J is proper by SUBSET_1:def 6;
hence I = J by A0, B1; :: thesis: verum

end;

hence I is max-ideal by A0, FILTER_2:def 8, SUBSET_1:def 6; :: thesis: verum