let L be Lattice; :: thesis: ( L is upper-bounded implies for I being Ideal of L st I <> the carrier of L holds
ex J being Ideal of L st
( I c= J & J is max-ideal ) )
assume L is upper-bounded ; :: thesis: for I being Ideal of L st I <> the carrier of L holds
ex J being Ideal of L st
( I c= J & J is max-ideal )
then A1: L .: is lower-bounded by LATTICE2:49;
let I be Ideal of L; :: thesis: ( I <> the carrier of L implies ex J being Ideal of L st
( I c= J & J is max-ideal ) )
assume I <> H₁(L) ; :: thesis: ex J being Ideal of L st
( I c= J & J is max-ideal )
then consider F being Filter of (L .:) such that
A2: ( I .: c= F & F is being_ultrafilter ) by A1, FILTER_0:18;
take .: F ; :: thesis: ( I c= .: F & .: F is max-ideal )
(.: F) .: = .: F ;
hence ( I c= .: F & .: F is max-ideal ) by A2, Th32; :: thesis: verum