let L be Lattice; :: thesis: for A being Filter of L holds
( not L = BooleLatt {{}} or A = {(Top L)} or A = <.L.) )
let A be Filter of L; :: thesis: ( not L = BooleLatt {{}} or A = {(Top L)} or A = <.L.) )
assume A0: L = BooleLatt {{}} ; :: thesis: ( A = {(Top L)} or A = <.L.) )
Top L = {{}} by A0, LATTICE3:4;
then reconsider B = {{{}}} as Filter of L by FILTER_0:12, A0;

per cases ( A = {} or A = {{},{{}}} or A = {{{}}} ) by lemma2, A0;

suppose A = {} ; :: thesis: ( A = {(Top L)} or A = <.L.) )

hence ( A = {(Top L)} or A = <.L.) ) ; :: thesis: verum

end;

suppose A = {{},{{}}} ; :: thesis: ( A = {(Top L)} or A = <.L.) )

hence ( A = {(Top L)} or A = <.L.) ) by lemma3, A0; :: thesis: verum

end;

suppose A = {{{}}} ; :: thesis: ( A = {(Top L)} or A = <.L.) )

hence ( A = {(Top L)} or A = <.L.) ) by A0, LATTICE3:4; :: thesis: verum

end;

end;