let L be Lattice; :: thesis: for p being Element of L st L is upper-bounded & p <> Top L holds
ex I being Ideal of L st
( p in I & I is max-ideal )
let p be Element of L; :: thesis: ( L is upper-bounded & p <> Top L implies ex I being Ideal of L st
( p in I & I is max-ideal ) )
assume L is upper-bounded ; :: thesis: ( not p <> Top L or ex I being Ideal of L st
( p in I & I is max-ideal ) )
then A1: ( L .: is lower-bounded & Bottom (L .:) = Top L ) by LATTICE2:49, LATTICE2:62;
assume p <> Top L ; :: thesis: ex I being Ideal of L st
( p in I & I is max-ideal )
then consider F being Filter of (L .:) such that
A2: ( p .: in F & F is being_ultrafilter ) by A1, FILTER_0:20;
take .: F ; :: thesis: ( p in .: F & .: F is max-ideal )
(.: F) .: = .: F ;
hence ( p in .: F & .: F is max-ideal ) by A2, Th32; :: thesis: verum