for L being Lattice st L is upper-bounded holds
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 )