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 :: thesis: for a being object st a in I holds
not a in F

let a be object ; :: 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 Th4; :: 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 Th25;
take G ; :: thesis: ( F c= G & G is ultra )

now :: thesis: not Bottom L in G

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 ;
hence ( F c= G & G is ultra ) by A1, Th22; :: thesis: verum