let L be non trivial Boolean Lattice; :: thesis: for A being Filter of L st L = BooleLatt {{}} & A = {(Top L)} holds
A is prime
let A be Filter of L; :: thesis: ( L = BooleLatt {{}} & A = {(Top L)} implies A is prime )
assume A1: ( L = BooleLatt {{}} & A = {(Top L)} ) ; :: thesis: A is prime
for H being Filter of L st A c= H & H <> the carrier of L holds
A = H

proof

let H be Filter of L; :: thesis: ( A c= H & H <> the carrier of L implies A = H )
assume ( A c= H & H <> the carrier of L ) ; :: thesis: A = H
then ( H = {} or H = {{{}}} ) by lemma3, A1, lemma2;
hence A = H by A1, LATTICE3:4; :: thesis: verum

end;

then A is being_ultrafilter by A1, FILTER_0:def 3;
hence A is prime by FILTER_0:45; :: thesis: verum