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

proof

assume that
A1: I <> H₁(L) and
A2: for J being Ideal of L st I c= J & J <> H₁(L) holds
I = J ; :: according to FILTER_2:def 8 :: thesis: I .: is being_ultrafilter
thus I .: <> H₁(L .: ) by A1; :: according to FILTER_0:def 3 :: thesis: for b₁ being Element of bool the carrier of (L .:) holds
( not I .: c= b₁ or b₁ = the carrier of (L .:) or I .: = b₁ )
let F be Filter of (L .:); :: thesis: ( not I .: c= F or F = the carrier of (L .:) or I .: = F )
.: F = F ;
hence ( not I .: c= F or F = the carrier of (L .:) or I .: = F ) by A2; :: thesis: verum

end;

assume that
A3: I .: <> H₁(L .: ) and
A4: for F being Filter of (L .:) st I .: c= F & F <> H₁(L .: ) holds
I .: = F ; :: according to FILTER_0:def 3 :: thesis: I is max-ideal
thus I <> H₁(L) by A3; :: according to FILTER_2:def 8 :: thesis: for J being Ideal of L st I c= J & J <> the carrier of L holds
I = J
let J be Ideal of L; :: thesis: ( I c= J & J <> the carrier of L implies I = J )
J .: = J ;
hence ( I c= J & J <> the carrier of L implies I = J ) by A4; :: thesis: verum