:: deftheorem Def6 defines /\/ FILTER_1:def 6 :
for L being Lattice
for F being Filter of L
for a being Element of L st L is I_Lattice holds
for b₄ being Element of (L /\/ F) holds
( b₄ = a /\/ F iff for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b₄ = Class (R,a) );