let L be Lattice; :: thesis: for p being Element of L st L is 0_Lattice & p <> Bottom L holds
ex H being Filter of L st
( p in H & H is being_ultrafilter )
let p be Element of L; :: thesis: ( L is 0_Lattice & p <> Bottom L implies ex H being Filter of L st
( p in H & H is being_ultrafilter ) )
assume that
A1: L is 0_Lattice and
A2: p <> Bottom L ; :: thesis: ex H being Filter of L st
( p in H & H is being_ultrafilter )
reconsider L9 = L as 0_Lattice by A1;
reconsider p9 = p as Element of L9 ;
p9 "/\" (Bottom L9) = Bottom L9 ;
then consider H being Filter of L such that
A3: ( <.p.) c= H & H is being_ultrafilter ) by A2, Th18, Th19;
take H ; :: thesis: ( p in H & H is being_ultrafilter )
p in <.p.) ;
hence ( p in H & H is being_ultrafilter ) by A3; :: thesis: verum