:: deftheorem Def9 defines (. FILTER_2:def 9 :
for L being Lattice
for D being non empty Subset of L
for b₃ being Ideal of L holds
( b₃ = (.D.> iff ( D c= b₃ & ( for I being Ideal of L st D c= I holds
b₃ c= I ) ) );