let L be Lattice; :: thesis: for A being Filter of L holds
( not L = BooleLatt {{}} or A = {} or A = {{},{{}}} or A = {{{}}} )
let A be Filter of L; :: thesis: ( not L = BooleLatt {{}} or A = {} or A = {{},{{}}} or A = {{{}}} )
assume A0: L = BooleLatt {{}} ; :: thesis: ( A = {} or A = {{},{{}}} or A = {{{}}} )
A <> {{}}

proof

assume Z0: A = {{}} ; :: thesis: contradiction
reconsider b = {{}}, a = {} as Element of L by TARSKI:def 2, A0, lemma3;
z1: {{}} /\ {} = b "/\" a by A0, LATTICE3:1;
( ( b in A & a in A ) iff b "/\" a in A ) by FILTER_0:8;
hence contradiction by z1, Z0, TARSKI:def 1; :: thesis: verum

end;

hence ( A = {} or A = {{},{{}}} or A = {{{}}} ) by A0, lemma1; :: thesis: verum