let L be non trivial Boolean LATTICE; :: thesis: for F being proper Filter of L ex G being Filter of L st
( F c= G & G is ultra )
let F be proper Filter of L; :: thesis: ex G being Filter of L st
( F c= G & G is ultra )
downarrow (Bottom L) = {(Bottom L)} by WAYBEL_4:23;
then reconsider I = {(Bottom L)} as Ideal of L ;

now

let a be set ; :: thesis: ( a in I implies not a in F )
assume a in I ; :: thesis: not a in F
then a = Bottom L by TARSKI:def 1;
hence not a in F by Th8; :: thesis: verum

end;

then I misses F by XBOOLE_0:3;
then consider G being Filter of L such that
A1: ( G is prime & F c= G ) and
A2: I misses G by Th29;
take G ; :: thesis: ( F c= G & G is ultra )

now

assume Bottom L in G ; :: thesis: contradiction
then not Bottom L in I by A2, XBOOLE_0:3;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then G is proper by Th8;
hence ( F c= G & G is ultra ) by A1, Th26; :: thesis: verum