:: deftheorem Def4 defines <. FILTER_0:def 4 :
for L being Lattice
for D being non empty Subset of L
for b₃ being Filter of L holds
( b₃ = <.D.) iff ( D c= b₃ & ( for F being Filter of L st D c= F holds
b₃ c= F ) ) );