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 A1: ( L is 0_Lattice & p <> Bottom L ) ; :: thesis: ex H being Filter of L st
( p in H & H is being_ultrafilter )
then reconsider L' = L as 0_Lattice ;
reconsider p' = p as Element of L' ;
p' "/\" (Bottom L') = Bottom L' by LATTICES:40;
then <.p.) <> the carrier of L by A1, Th23;
then consider H being Filter of L such that
A2: ( <.p.) c= H & H is being_ultrafilter ) by A1, Th22;
take H ; :: thesis: ( p in H & H is being_ultrafilter )
p in <.p.) ;
hence ( p in H & H is being_ultrafilter ) by A2; :: thesis: verum