let L be Lattice; :: thesis: for A being Filter of L st L = BooleLatt {{}} & A is being_ultrafilter holds
A = {(Top L)}
let A be Filter of L; :: thesis: ( L = BooleLatt {{}} & A is being_ultrafilter implies A = {(Top L)} )
assume A0: L = BooleLatt {{}} ; :: thesis: ( not A is being_ultrafilter or A = {(Top L)} )
assume Z1: A is being_ultrafilter ; :: thesis: A = {(Top L)}
A1: Top L = {{}} by A0, LATTICE3:4;
then reconsider B = {{{}}} as Filter of L by FILTER_0:12, A0;
Z2: not {} in A

proof

assume {} in A ; :: thesis: contradiction
then Bottom L in A by A0, LATTICE3:3;
hence contradiction by Z1, LOPCLSET:29, A0; :: thesis: verum

end;

A <> {{},{{}}} by Z2, TARSKI:def 2;
hence A = {(Top L)} by A1, lemma2, A0; :: thesis: verum