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 A1: ( I <> H₁(L) & ( for J being Ideal of L st I c= J & J <> H₁(L) holds
I = J ) ) ; :: according to FILTER_2:def 10 :: thesis: I .: is being_ultrafilter
hence I .: <> H₁(L .: ) ; :: according to FILTER_0:def 4 :: thesis: for b₁ being Filter 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 A1; :: thesis: verum

end;

assume A2: ( I .: <> H₁(L .: ) & ( for F being Filter of L .: st I .: c= F & F <> H₁(L .: ) holds
I .: = F ) ) ; :: according to FILTER_0:def 4 :: thesis: I is_max-ideal
hence I <> H₁(L) ; :: according to FILTER_2:def 10 :: 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 A2; :: thesis: verum